The Specification Logic sHML¶

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 Hennessy-Milner 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 and tt denote falsity and truth respectively,
X is a logical variable,
The maximal fix-point construct specifies recursion via the logical variable X and binds the free occurrences of X in the sub-formula φ, and,
and(...) is a sequence of comma-separated conjunctions where each conjunct is a sub-formula φᵢ 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 pattern-matching 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
Short-circuit 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₁, P₂, P₃, and P₄ stated informally can be expressed in sHML.

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

Operator	Description
`not`	Unary logical NOT
`and`	Logical AND
`or`	Logical OR
`xor`	Logical XOR