The Specification Logic¶
Overview¶
For the sake of simplicity, the script hello_prop.hml
used in our hello world example specifies a sHML property that every system necessarily violates, namely, the formula ff
that denotes falsity.
We now look at the full sHML grammar that enables us to express more interesting and useful properties about programs (not traces).
Specifications in sHML—also called formulae—are interpreted over the states of transition models of programs we wish to analyse.
sHML is a syntactic subset of the more expressive HennessyMilner Logic with recursion, and is used to specify safety properties.
Recall safety properties state that “something bad should never happen”.
sHML formulae are generated from the following grammar:
φ ∈ sHML ::= ff  tt (1)
 X (2)
 max(X. φ) (3)
 and([α₁]φ₁, ..., [αₙ]φₙ) (4)

Formulae
ff
andtt
denote falsity and truth respectively, 
X
is a logical variable, 
The maximal fixpoint construct specifies recursion via the logical variable
X
and binds the free occurrences ofX
in the subformulaφ
, and, 
and(...)
is a sequence of commaseparated conjunctions where each conjunct is a subformulaφᵢ
guarded by the universal modal operator[αᵢ]
(also called a necessity).
To handle reasoning over program event data, the modal operator is equipped with symbolic actions α
of the form P when C
, where P
is an event pattern and C
, a decidable Boolean constraint.
Patterns correspond to events that the program under analysis exhibits.
These patterns contain data variables that are instantiated with values learnt at runtime from matched events.
Pattern variables bind the free variables in constraints C
, and this binding scope extends to the continuation formula φ
.
Symbolic action patterns follow the patternmatching syntax of Erlang and Elixir, where atoms are matched directly, and the ‘don’t care’ pattern _
matches any data value.
Central to the conjuncted necessities construct, and([α₁]φ₁, ..., [αₙ]φₙ)
, is the constraint that at any one point in time, at most one conjunct [αᵢ]φᵢ
may be satisfied.
This enables detectEr to synthesise deterministic analyser code [Refs:Antoins,IAN,TutPaper].
We say that a program (or a program state) satisfies the formula [P when C]φ
whenever it exhibits an event that matches pattern P
, fulfils the constraint C
, and the ensuing program behaviour then satisfies φ
.
When the constraint is true
, the expression when C
may be omitted for readability.
Pattern and constraint expressions¶
detectEr supports five event patterns describing the lifecycle of processes.
A fork
action is exhibited by a process when it spawns a new child process; its dual, init
, is exhibited by the corresponding child upon initialisation.
Process exit
actions signal termination, while send
and recv
describe process interaction.
Program event  Event pattern  Pattern variable  Description 

fork 
P₁ → P₂ , Mod :Fun (Args ) 
P₁ 
PID of the parent process spawning P₂ 
P₂ 
PID of the child process spawned by P₁ 

Mod :Fun (Args ) 
Function signature consisting of the module, function and arguments  
init 
P₁ ← P₂ , Mod :Fun (Args ) 
P₁ 
PID of the parent process spawning P₂ 
P₂ 
PID of the child process spawned by P₁ 

Mod :Fun (Args ) 
Function signature consisting of the module, function and arguments  
exit 
P₁ ** Reason 
P₁ 
PID of the terminated process 
Reason 
Termination reason  
send 
P₁ : P₂ ! Msg 
P₁ 
PID of the process issuing the message 
P₂ 
PID of the recipient process  
Msg 
Message payload  
recv 
P₂ ? Msg 
P₂ 
PID of the recipient process 
Msg 
Message payload 
The variables P₁
and P₂
in event patterns must be a port ID or PID, whereas Reason
and Msg
may be any Erlang data type, i.e., one of atom, Boolean, integer, float, string, bit string, reference, fun, port ID, PID, tuple, map, and list.
Mod
and Fun
must be atoms, and Args
, an arbitrary list comprised of the aforementioned data types.
Pattern matching
Our current detectEr syntax does not yet implement full Erlang pattern matching, including $, map, record and bit string expressions; these will be added in future releases of the tool.
Note that these data values can still be used in patterns, so long as the pattern matching expression does not unwrap the individual data components of these values.
For instance, the pattern Var = Map
is acceptable whereas #{K := V} = Map
is not; similarly, Var = List
may be used but not [$d, $a  _] = List
.
Constraint definitions on pattern variables used by detectEr correspond to Erlang guard sequences consisting of guard expressions. The set of valid Erlang guards supported by detectEr are the following:
 Variables.
 Values, i.e., atom, Boolean, integer, float, string, bit string, reference, fun, port ID, PID, tuple, map, and list.

Expressions constructing atoms, integer, floats, lists, and tuples.

Term comparisons.
Operator Description ==
Equal to /=
Not equal to =<
Less than or equal to <
Less than >=
Greater than or equal to >
Greater than =:=
Exactly equal to =/=
Exactly not equal to 
Arithmetic expressions.
Operator Description Argument Type +
Unary addition Number 
Unary subtraction Number +
Addition Number 
Subtraction Number *
Multiplication Number /
Floating point division Number bnot
Unary bitwise NOT Integer div
Integer division Integer rem
Integer remainder of X/Y Integer band
Bitwise AND Integer bor
Bitwise OR Integer bxor
Arithmetic bitwise XOR Integer bsl
Arithmetic bit shift left Integer bsr
Bit shift right Integer 
Boolean expressions.
Operator Description not
Unary logical NOT and
Logical AND or
Logical OR xor
Logical XOR 
Shortcircuit expressions
andalso
,orelse
.
A simple example¶
Let us try to specify a safety requirement on the behaviour of our calculator program.
The sHML formula with symbolic action Srv:Clt ! {bye, Tot} when Tot < 0
describes the property requiring that “the program state does not exhibit a send event whose payload consists of {bye, Tot}
with a negative total:
and([Srv:Clt ! {bye, Tot} when Tot < 0])ff
Recall that the universal modality states that, for any program event satisfying the symbolic action P when C
in [P when C]φ
, the ensuing program behaviour must then satisfy the continuation formula φ
.
However, no program state can satisfy the continuation ff
!
This means that the formula and([Srv:Clt ! {bye, Tot} when Tot < 0])ff
can only be satisfied when our calculator program does not exhibit the event described by the symbolic action Srv:Clt ! {bye, Tot} when Tot < 0
.
Suppose our server with PID <0.10.0>
exhibits the send
event <0.10.0>:<0.16.0> ! {bye, 1}
in response to a request issued by a client with PID <0.16.0>
.
It matches pattern Srv:Clt ! {bye, Tot}
, instantiating the variables Srv = <0.10.0>
, Clt = <0.16.0>
, and Tot = 1
.
The constraint when Tot < 0
is also satisfied by Tot
, leading to a violation, i.e., ff
.
For a different send
event <0.10.0>:<0.16.0> ! {bye, 1}
, the symbolic action in the modality [Srv:Clt ! {bye, Tot} when Tot < 0]
is not satisfied, and consequently, and([Srv:Clt ! {bye, Tot} when Tot < 0])ff
is not violated.
Analogously, the exit
event <0.10.0> ** killed
does not lead to a violation of the formula since the pattern Srv:Clt ! {bye, Tot}
fails to match the event shape.
Cheat sheet
The formula [α]ff
means that the program must not perform the symbolic action α
.
We next learn how the safety properties P_{1}, P_{2}, P_{3}, and P_{4} stated informally can be expressed in sHML.