The Abstract Model

Soter derives a finitely representable over-approximation of the execution of the input Erlang module. This abstract model of the program is called an Actor Communicating System (ACS).

An ACS can be read as a "decorated" control-flow graph but in fact it is interpreted by Soter (and BFC) as an infinite-state system, equivalent to a Vector Addition System (VAS) or, equivalently, a Petri net.

How to read the diagrams

An ACS transition rule has the shape

\[\pid : q \xrightarrow{\ell} q'\]

which means that a process of pid class \(\pid\) can transition from state \(q\) to state \(q'\) with (possible) communication side effect \(\ell\), of which there are four kinds, namely,

  1. the process makes an internal transition

  2. it extracts and reads a message \(msg\) from its mailbox

  3. it sends a message \(msg\) to a process of pid class \(\pid'\)

  4. it spawns a process of pid class \(\pid'\).

The various kinds of control states and transitions are represented pictorially as follows.

Explanation of elements of an ACS diagram [open]