Process Calculus

Formal Model of Business Process Engine

Intro

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.

Process Encoding


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.

Process Modality


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.2.2.2.1 trace (p: process): storage (signature p) = p.2.2.2.2

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))

Applications

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.