Tutorial Enabling Analysis: Difference between revisions

The B-method and in particular its successor Event-B are methodologies for formal development and verification of systems. In Event-B, a machine is usually viewed as a reactive system executing continuously enabled (atomic) events in an interleaved fashion. Thus, parallel events of the system are easily modeled as an interleaving of operation executions. On the other hand, the introduction of abstract counters is required when events are supposed to be executed in some (sequential) order. This, however, can in some cases slow the work of understanding and verifying a model since identifying the sequential ordering of events in an Event-B model is not that obvious. Thus, using methods for determining the control flow can be sometimes very beneficial for understanding the model, as well as for techniques for automatic verification such as model checking.

In this tutorial we present a static analysis for B and Event-B that can be used to reveal the control flow of a machine and to optimize model checking of models written in B and Event-B (see also Tutorial on Partial Guard Evaluation ). The results of the analysis, designated also as ‘’enabling analysis’’, can be presented as relations by means of a table or by means of a graph. For simplicity, we will concentrate mainly on B and use the terminology of the formalism.

Enabling Relation

What we want to find out is how the operations influence each other within a B model. In other words, for each pair (op1,op2) of operations we try to determine as precise as possible how op1 can affect the guard condition of op2 with regard to enabledness. To determine the enabling relations between operations we use syntactic analyses, as well as the constraint-based abilities of ProB.

Consider the following B machine:

MACHINE Example
VARIABLES x, y, z
INVARIANT
    x:NATURAL
  & y:INTEGER
  & z:INTEGER
INITIALISATION 
  x:=6 || y:=-2 || z := 0
OPERATIONS
  Op1 = PRE x + y >= 4  THEN x:=x+2 || y:=2 END;
  Op2 = PRE x mod 2 = 1 THEN x:=x+1 || y:=2 END;
  Op3 = PRE x mod 2 = 0 THEN x:=x+2 END;
  Op4 = PRE x<0 THEN y:=y-1 END;
  Op5 = PRE y/=2 THEN z:=3 END
END

The machine has three variables x,y,z, where x ranges over the domain of natural numbers and y and z over the domain of all integers. For this machine we have 25 pairs of operations for which we want to determine the respective enabling relations. Additionally, we identify 5 further pairs that show the influence of the INITIALISATION on all other operations. Consider, for example, the pair (Op2,Op1) in Example.mch. Clearly, Op1 is enabled in each state of Example.mch where the predicate ‘x+y>=4’ is fulfilled. Since the effect of Op2 assigns 2 to y and increments x by one upon condition that x is a positive odd number in the before-state of Op2, we can assume that Op1 is always enabled after the execution of Op2. In other words, in all after-states of Op2 the operation Op1 is guaranteed to be enabled. This relation between Op2 and Op1 we can illustrate as follows:

In the figure above the green boxes denote that the evaluation of the guard of Op1 is true, whereas the red boxes denote that the evaluation of the guard of Op1 is false.

Another pair of interest is (Op2,Op5) in Example.mch. Clearly, Op5 is enabled only in those states in which y is not equal to 2. Obviously, in each after-state of Op2 y is equal to 2 and thus we can conclude that Op5 is impossible to be enabled after each execution of Op2. Such a relation between two operations we denote as ‘’impossible’’ and can be illustrated as follows:

Both arrows in the illustration of the ‘’impossible’’ relation indicate that whether the guard condition of Op5 is fulfilled or not in a before-state of Op2 operation Op5 will be disabled in the respective after-state of Op2. In order to recognize a tuple (op1,op2) as ‘’impossible’’ we require that op2 is always disabled after op1 without further considering whether op2 is always enabled or always disabled in the before-states of op1.

Consider, for instance, the pair (Op2, Op2) in the machine above. We can easily conclude that Op2 becomes disabled after it is executed and clearly, the second case (\false -> \false) of the impossible relation is not possible for (Op2, Op2). This gives rise of introducing another (more specific) impossible relation:

Accordingly, we can derive another relation from ‘’impossible’’ for which only the second case of the ‘’impossible’’ relation is fulfilled:

As an example for a pair of operations that fulfills the ‘’impossible_keep’’ requirement you can take, for example, the tuple (Op3,Op2) from the Example machine. Since Op2 and Op3 cannot be both enabled in a state and the execution of Op3 cannot enable Op2, then we can easily conclude that Op2 remains always disabled after Op3.

Similarly as for ‘’impossible’’, one could derive two further enabling relations from ‘’guaranteed’’:

Another interesting class of enabling relations that could be helpful for better understanding and analyzing B and Event-B models is that of the ‘’keep’’ relations. We say that an operation op1 ‘’keeps’’ another operation op2 if op1 cannot change the status of the enabling condition of op2, i.e. op1 keeps op2 enabled respectively disabled. This relationship could be illustrated as follows:

Examples of pairs in Example.mch that are elements of the keep relation are, for example, the tuples (Op1,Op2) and (Op1,Op3). ‘’keep’’ relations can sometimes be easily determined by analyzing just the syntactic structure of both operations, or more precisely the “read” and “write” sets of both operations.^[1] If, for example, an operation op1 does not write any variable of the machine that is read in the guard condition of op2, then we can infer that op1 ‘’keeps’’ op2. In that case we also say that op1 does not change op2 syntactically. In the class of the ‘’keep’’ relations are included also relations such as independence. Two operations op1 and op2 are called independent if each of them cannot disable the other operations and the both orders of execution <op1,op2> and <op2,op1> have the same effect.^[2]

All three classes (‘’guaranteed’’, ‘’impossible’’ and ‘’keep’’) of enabling relations presented so far represent definite relations. That is, if a pair of operations (op1,op2) is confirmed to be a relation of one of this three classes, then we can certainly say what effect on the enabling condition of op2 would the execution of op1 have. However, for some pairs of operations we cannot certainly say what effect an operation would have on the enabling condition of another operation. This is due to the fact that the enabling status of an operation does not only depend on the effect of the executed operations, but also on the current variables’ evaluation. Take, for instance, the tuple (Op3,Op1) from the B machine above. Considering the action part of Op3 and the guard condition of Op1 we can assume that Op3 can enable Op1. Since the guard of Op1 depends not only on the current value of x, but also on y, there could be transitions s${\displaystyle {\overset {Op_{3}}{\rightarrow }}}$s' in the state space of the machine where Op1 is disabled in both states ‘’s’’ and ‘’s’’’. Though, what we could definitely say is that Op3 cannot disable Op1. This relationship we can illustrate as follows:

The opposite relation of “possible_enable” is the relation where an operation op2 can disable another operation op1. Formally, we say that op2 can disable op1 if op2 may disable op1 and op2 cannot enable op1. This relationship is denoted as “possible_disable” and can be illustrated as follows:

In order to determine how operations influence each other we need to assure first that these are feasible. An operation ‘’op’’ is said to be feasible if there is a state of the machine that satisfies the invariant of the machine and in which ‘’op’’ is enabled. In the B machine above the operation Op4, for example, is not feasible. Obviously, Op4 is enabled only in states where x is a negative number and states in which x is a negative number are visibly not consistent with the invariant since "x : NATURAL". Such incompatibilities are sometimes of great importance for the modeler and therefore they should be revealed in the process of computing the enabling relations. In our case for each pair of operations (Op4,-) and (-,Op4) the status “infeasible” will be returned.

We can now list all possible enabling relations for the machine Example.mch by means of a table. For each entry in the table the operation in the row is the operation whose effect is studied on the status of the guard of the operation in the column.