Skip to content

The Specification Logic maxHML

Overview

maxHML enables us to express properties on the executions of programs. Like sHML, maxHML is a another syntactic subset of the more expressive Hennessy-Milner Logic with recursion. It is used to express safety properties, but by contrast to the sHML fragment of The Specification Logic sHML, maxHML is interpreted over executions (called traces), rather than process execution graphs. maxHML formulae are generated from the following grammar:

φ, ψ ∈ maxHML ::=  ff  |  tt             (1)
       |  <α>φ                           (2)
       |  [α]φ                           (3)
       |  φ or ψ                         (4)
       |  φ and ψ                        (5)
       |  X                              (6)
       |  max(X. φ)                      (7)

  1. Formulae ff and tt denote falsity and truth respectively,

  2. <α>φ is the existential modal operator guarding the continuation formula φ (also called a possibility),

  3. [α]φ, the dual of <α>φ, is the universal modal operator guarding the continuation formula φ (also called a necessity),

  4. φ or ψ is a disjunction,

  5. φ and ψ is a conjunction,

  6. X is a logical variable, and,

  7. max(X. φ) is the greatest fixed point construct that specifies recursion via the logical variable X and binds the free occurrences of X in the sub-formula φ.

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.

We say that a trace satisfies the formula <P when C>φ when it exhibits an event that matches pattern P, fulfils the constraint C, and the ensuing program behaviour also satisfies φ. Dually, a trace satisfies [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 traces of our token server program.

The maxHML formula with symbolic action Prnt ← Srv, token_server:loop([OwnTok, _]) when OwnTok =/= 1 describes the property requiring that “the server does not start with an identifier token other than 1”.

[Prnt ← Srv, token_server:loop([Tok]) when Tok =/= 1]ff

Recall that the universal modality states that, for any program event satisfying the symbolic action P when C in [P when C]φ, the rest of the trace must then satisfy the continuation formula φ. However, no trace continuation can satisfy the formula ff! This means that the [Prnt ← Srv, token_server:loop([OwnTok, _]) when OwnTok =/= 1]ff can only be satisfied when our trace does not exhibit the event described by the symbolic action Prnt ← Srv, token_server:loop([OwnTok, _]) when OwnTok =/= 1.

Suppose our server with PID <0.10.0> exhibits the init event <0.16.0> ← <0.10.0>, token_server:loop([-1, 0]) when launched by a parent process with PID <0.16.0>. It matches pattern Prnt ← Srv, token_server:loop([OwnTok, _]) when OwnTok =/= 1, instantiating the variables Srv = <0.10.0>, Prnt = <0.16.0>, and OwnTok = -1. The constraint when OwnTok =/= 1 is also satisfied, leading to a violation, i.e., ff.

For a different init event <0.16.0> ← <0.10.0>, token_server:loop([1, 0]), the symbolic action in the modality [Prnt ← Srv, token_server:loop([OwnTok, _]) when OwnTok =/= 1] is not satisfied, and consequently, [Prnt ← Srv, token_server:loop([OwnTok, _]) when OwnTok =/= 1]ff is satisfied. Analogously, the init event <0.16.0> ← <0.10.0>, calc_server:loop() satisfies the formula since the pattern Prnt ← Srv, token_server:loop([Tok]) fails to match the event shape.

Cheat sheet

The formula <α>tt means that it is possible for the trace to exhibit the symbolic action α. Dually, [α]ff states that the trace must not exhibit the symbolic action α.

You should try expressing the safety properties P1, P2, and P3 stated informally in the Getting Started section in terms of maxHML. Keep in mind that now, our formal model is the set of traces generated by the program, rather than the program transition graph itself.

We next learn how runtime monitors can be synthesised from maxHML.