Formalising Properties

---

Choosing what to analyse

detectEr provides the keywords with and monitor to target program processes for a particular sHML specification. The with keyword picks out the signature of the function that is spawned as a process, whereas the monitor keyword defines the property to be runtime analysed. For example, to verify the behaviour of our calculator process against a sHML formula φ, we write:

with
  calc_server:loop(_)
monitor
  φ

From an instrumentation standpoint, with establishes the set of trace events corresponding to the program process it targets, thus enabling the specification to abstract from the events that are generated by other processes. This helps maintain the size of sHML specifications compact whenever possible. In using with, our formula need not account for superfluous trace events (e.g. of another calculator process) that tend to make the specification exercise tedious and error-prone.

Let us formalise the properties from the Getting Started section; these are specified with respect to the five process events fork, init, exit, send, and recv supported by detectEr. We include our calculator server transition model for reference.

Formalising P₁

(P₁)    The service request count returned on shutdown is never negative.

P₁ is an extension of the property that we have already seen earlier, and([Srv:Clt ! {bye, Tot} when Tot < 0])ff, that requires the program state “not to exhibit a send event whose payload consists of {bye, Tot} where Tot is negative.” While in principle, this sHML formula is correct, it does not account for the other program events that our calculator server can exhibit from one of its states. For example, from Q0, the server exhibits recv events that are ignored by the formula; similarly, from Q2, the server transitions with a send event to Q1, but the message payload is not the one we are after. We remedy this by adding clauses that handle these possibilities.

with
  calc_server:loop(_)
monitor
  and([Lnc <- Srv, calc_server:loop(Args)]
    max(X.
      and(
        [Srv ? Clt]X,
        [Srv:Clt ! {bye, Tot} when Tot < 0]ff,
        [Srv:Clt ! {Ack, Ans} when Ack =:= ok orelse (Ack =:= bye andalso Ans >= 0)]X
      )
    ).

Using with .. monitor, we designate the spawned calculator server loop function calc_server:loop/1 as the process to be analysed against the formalisation of property P₁ (lines 1-3). Our formalisation of P₁ consists of two conjuncted necessities, i.e., and(...). The first conjuncted necessity on line 4 handles the init event exhibited by every process upon initialisation (we remark that init was elided in the transition model of our calculator server to simplify our discussion, but we need to account for it!). The second nested and(...) on line 6 includes the additional necessities that cover the other possible events produced by the transition system above, recursing on the fix-point variable X (lines 7 and 9). Line 8 shows our earlier formula [Srv:Clt ! {bye, Tot} when Tot < 0]ff that then checks for the condition imposed by P₁.

There are a couple of comments that are in order. First, the constraints on lines 8 and 9 ensure mutual exclusivity between the two necessities, i.e., either Tot < 0 or, Ans >= 0 only when the acknowledgement is the atom bye. Second, you may observe that the sub-formula on line 8 alone seems to capture the core requirement of property P₁. This line of reasoning is partially right. However, to interpret the requirement stated informally (in English) by P₁ and formalise it unambiguously, one must take the transition model into account. In fact, formalising P₁ for a different transition system potentially yields a specification that is altogether unlike the one above for our calculator server. Specific to our transition model, the necessities on lines 7 and 9 act as filters that ‘eat up’ the non-relevant program events.

Note

Variables Lnc, Srv, and Clt in our formalisation of P₁ are included assist in our explanation, but can be replaced with the don’t care pattern _ since these are unused in constraints. We omit such variables going forward.

Reformulating P₁

P₁ safeguards against the calculator returning a negative request total when shut down. An examination of calc_server:loop/1 promptly reveals that a non-negative request total returned on server shutdown does not necessarily mean that the number of tracked client requests is correct. In fact, starting the server loop with any number other than 0 will always yield an incorrect request total. Let us rectify this oversight by reformulating P₁.

(P’₁)    The initial service request count must be 0.

Its corresponding formalisation leverages the init event pattern, simplifying the formula considerably:

with
  calc_server:loop(_)
monitor
  and([_ <- _, calc_server:loop([Tot]) where Tot =/= 0]ff).

Line 4 consists of the singleton conjuncted necessity where the event pattern matches the spawned function against the module and function name atoms, calc_server and loop, respectively. The list pattern [] matches the argument list containing exactly one argument whose must be 0.

Formalising P₂

(P₂)    Replies are always sent to the client indicated in the request.

P₂ describes a fragment of the client-server protocol, asserting that server replies are always addressed to the clients issuing them. Unlike the properties seen thus far, this requirement induces data dependency between client requests and server responses.

with
  calc_server:loop(_)
monitor
  and([_ <- _, calc_server:loop(_)]
    max(X. 
      and([Srv_1 ? {Clt_1, _}]
        and(
          [Srv_2:Clt_2 ! _ when Srv_1 =:= Srv_2 andalso Clt_1 =/= Clt_2]ff,
          [Srv_2:Clt_2 ! _ when Srv_1 =:= Srv_2 andalso Clt_1 =:= Clt_2]X
        )
      )
    )
  ).  

Our formalisation of P₂ expresses this data dependency in the nested formulae above via the binders Srv_1 and Clt_1, that are used in the constraint of the sub-formulae on lines 8 and 9. Srv_1 =:= Srv_2 scopes our reasoning to single server instance, i.e., the same calculator server process. The formula is violated when Clt_1 =/= Clt_2 (since the continuation would need to satisfy ff), and recurs on variable X otherwise. Recall that the comparisons between the different variable instantiations is possible since the binding scope of the event pattern variables Srv_1 and Clt_1 in the outer necessity extends to the context of the inner and(...) on lines 7-10.

Refining P₂

The formalisation of P₂ above does not account for the case where the server interacts with more than one client. It disregards the possibility of interleaved execution, which is inherent to concurrent settings where processes are unable to control when messages are received. For instance, while the sub-formula [Srv_1 ? {Clt_1, _}] on line 6 matches an initial recv event, an ensuing recv event (e.g. due to a second client that happens to interact with the server) satisfies neither of the necessities on lines 8 and 9. This does not reflect the requirement of our original property P₂, and is yet another manifestation of the issue encountered earlier, i.e., formalising a property must be done in connection to the context in which the program operates. We handle this inconvenience by augmenting the formula to filter non-relevant events, as previous.

with
  calc_server:loop(_)
monitor
  and([_ <- _, calc_server:loop(_)]
    max(X.
      and([Srv_1 ? {Clt_1, _}]
        max(Y.
          and(
            [Srv_2:Clt_2 ! _ when Srv_1 =:= Srv_2 andalso Clt_1 =/= Clt_2]ff,
            [Srv_2:Clt_2 ! _ when Srv_1 =:= Srv_2 andalso Clt_1 =:= Clt_2]X,
            [_ ? _]Y
          )
        )
      )
    )
  ).

Formalising P₃

(P₃)    A request for adding two numbers always returns their sum.

P₃ demonstrates how we can use constraints to perform more complex reasoning on program event data, besides equality and range checks.

with
  calc_server:loop(_)
monitor
  and([_ <- _, calc_server:loop(_)]
    max(X.
      and([_ ? {_, {add, A, B}}]
        and(
          [_:_ ! {ok, Res} when Res =/= A + B]ff,
          [_:_ ! {ok, Res} when Res =:= A + B]X
        )
      )
    )
  )

This sHML formula compares the result issued by the server, instantiated in the variable Res, against the sum of the values instantiated in A and B. Necessity [_ ? {_, {add, A, B}}] on line 6 corresponds to the server receiving and addition request from a client, consisting of the payload {add, A, B}. A and B are added and compared to the server result embedded in the payload of the send event exhibited by the server in the nested necessities on lines 8 and 9. The first sub-formula (line 8) handles the case where the addition is incorrectly executed by the server, whereas the second sub-formula (line 9) is satisfied when the addition is correct, unfolding the formula via recursion on variable X.

Formalising P₄

(P₄)    Client requests are never serviced more than once.

P₄ specifies a control aspect of the client-server interaction. The corresponding sHML formula expresses this requirement via a guarded fix-point that recurs on X for sequences of send-recv events. This recursion captures normal server operation that corresponds to the sub-formula on line 5 followed by the one on line 7, and then [_ ? _]X on line 10 followed thereafter by the sub-formula of line 7.

with
  calc_server:loop(_)
monitor
  and([_ <- _, calc_server:loop(_)]
    and([_ ? _]
      max(X.
        and([Srv_1:Clt_1 ! _]
          and(
            [Srv_2:Clt_2 ! _ when Srv_1 =:= Srv_2 andalso Clt_1 =:= Clt_2]ff,
            [_ ? _]X
          )
        )
      )
    )
  ).

Our formula is violated when a send event matched by [Srv_1:Clt_1 ! _] is followed by a second send that is matched by the sub-formula on line 9. The constraint Clt_1 =:= Clt_2 of the necessity on line 9 ensures that duplicate send events concern the same recipient.

---

Having formalised properties P₁, P₂, P₃, and P₄, we are now in a position to use detectEr and synthesise the corresponding analysers in Erlang code. But before doing that, we need to discuss how the runtime setting limits our view of program behaviour, and how analysers fit in the picture.