Skip to content

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 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)
  1. Formulae ff and tt denote falsity and truth respectively,

  2. X is a logical variable,

  3. The maximal fix-point construct specifies recursion via the logical variable X and binds the free occurrences of X in the sub-formula φ, and,

  4. 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 P1, P2, P3, and P4 stated informally can be expressed in sHML.