Process Calculus defines formal business process engine that coule be mapped onto Synrc/BPE Erlang/OTP application or OCaml Lwt library with Coq.io front-end. Here is given Erlang approach for modeling processes.
We will describe process calculus as formal model of two types: 1) the general abstract MLTT interface of process modality that can be used as formal bindings to low-level programming or as a top-level interface; 2) the low-level formal model of Erlang/OTP generic server.
According to MLTT for declaring a type means formally define its formation rule or type former, sole introduction rule, a lot of elims (projections and modality morphisms, recursor and induction) and beta and eta computational equalities. In this article we formally define process modality and will end up with two examples: Erlang/OTP generic server process and Synrc/BPE application.
Definition (Storage). The secure storage based on verified cryptography. NOTE: For simplicity let it be a compatible list.
storage: U -> U = list
Definition (Process). The type formation rule of the process is a $\Sigma$ telescope that contains: i) protocol type; ii) state type; iii) in-memory current state of process in the form of cartesian product of protocol and state which is called signature of the process; iv) monoidal action on signature; v) persistent storage for process trace.
process : U = (protocol state: U) * (current: prod protocol state) * (act: id (prod protocol state)) * (storage (prod protocol state))
Definition (Spawn). The sole introduction rule, process constructor is a tuple with filled process type information. Spawn is a modal arrow representing the fact that process instance is created at some scheduler of CPU core.
spawn (protocol state: U) (init: prod protocol state) (action: id (prod protocol state)) : process = (protocol,state,init,action,nil)
Definition (Accessors). Process type defines following accessors (projections, this eliminators) to its structure: i) protocol type; ii) state type; iii) signature of the process; iv) current state of the process; v) action projection; vi) trace projection.
protocol (p: process): U = p.1 state (p: process): U = p.2.1 signature (p: process): U = prod p.1 p.2.1 current (p: process): signature p = p.2.2.1 action (p: process): id (signature p) = p.126.96.36.199 trace (p: process): storage (signature p) = p.188.8.131.52
NOTE: the are two kinds of approaches to process design: 1) Semigroup: $P \times S \rightarrow S$; and 2) Monoidal: $P \times S \rightarrow P \times S$, where P is protocol and S is state of the process.
Definition (Receive). The modal arrow that represents sleep of the process until protocol message arrived.
receive (p: process) : protocol p = axiom
Definition (Send). The response free function that represents sending a message to a particular process in the run-time. The Send nature is async and invisible but is a part of process modality as it's effectfull.
send (p: process) (message: protocol p) : unit = axiom
Definition (Execute). The Execute function is an eliminator of process stream performing adding single entry to the secured storage of the process. Execute is a transactional or synchronized version of asynchronous Send.
execute (p: process) (message: protocol p) : process = let step: signature p = (action p) (message, (current p).2) in (protocol p, state p, step, action p, cons step (trace p))
1) Run-time formal model of Erlang/OTP compatible generic server and with extraction to Erlang. This is example of process modality usage at low-level. The run-time formal model could be seen here streams.
2) Formal model Business Process Engine application that runs on top of Erlang/OTP extracted model. The Synrc/BPE model could be seen here bpe.
3) Formal model of Synrc/N2O application and n2o_async in particular.