5. Modeling
5.1 Verifying General Specifications
We use NuSMV to verify whether the SYN-sequence satisfy the given specifications.
Our system can translate the SYN-sequence into the NuSMV model language and run the NuSMV automatically. So far the temporal specifications have to be input manually, and they are parsed by the NuSMV. The details of NuSMV are described in [63]. Figure 5.1 shows the verification scheme.
Figure 5.1. The scheme for verification with specification in Type I.
For example, if we have a SYN-sequence given in Figure 3.3 and we want to know whether the value of variable remains 4 or 7 before variable being accessed and whether event 1 of process 1 always happens before event 3 of process 0 (see page 18).
Let’s see how to translate the SYN-sequence given in Figure 3.3. The behavior of each SYN-
sequence
Stateful Translator
Stateful Model
NuSMV Specifications
(Type I)
false + counterexample true
process is described in separate module. These modules are process modules. The NuSMV module that models process 0 is
MODULE seq0(prc, aVer, bVer)
In this module, we declare a variable evnt in VAR section to indicate which event of this process is lastly executed before this state. In the right hand side of the colon gives the domain of this state variable. There are two imaginary events, say, -1 and 4 standing for initial and terminated states of the process respectively. Thus before any events being executed, we can leave our process in the state where evnt = -1, whereas let our process sunk in the state where evnt = 4 when all events in the SYN-sequence has been executed. Note that we have only four events so that the last event is numbered 3 here. ASSIGN segment comprises the assignments of variables. It is obvious that init(evnt) := -1; assigns -1 to the initial value of evnt and next() represents
the next value of a variable. This will be further constrained in the TRANS section and in the main module and will be discussed there.
The case analysis uses the keywords case and esac to enclose it. Each statement in the case analysis sequentially comprises a Boolean expression for the condition, a colon, and the return value, and ends with a semicolon. When evaluating the case analysis, the first return value in the statement where the Boolean expression evaluated to be true is returned to the identifier outside the case analysis. Then this case analysis is finished.
The variables aVer and bVer keep the version numbers of share variables and respectively. Their value is modified only when the event does write operation to that variable and all access to that variable of previous version has been done. For example, version 2 is written into the variable in event 3 of process 0, hence the next value of aVer is changed to 2 when event 2 has been executed and aVer is 1. The requirement that all access to that variable of previous version has been done seems not satisfied if we concern only two states; hence we add the TRANS constraints to force all transitions follow the execution behavior of the SYN-sequence. Since all states and transitions must satisfy all constraints in NuSMV, we are confident that the requirement to write a share variable is met. The rule for this requirement is similar to the Dependency Algorithm and will be further discussed later.
We will generalize the transitional behavior of this module now. The events proceed according to the latest version number of variable which will be accessed, e.g. event 2 in process 0 can proceed only if the version number of is 1 before next state. This is natural since this event is to read variable of version 1. Event 3 in process 0, however, can proceed only if the version number of is 1 since it writes to version 2. This,
along with the transitions of version number of each variable, follows a rule in the following which is similar to Dependency Algorithm.
Transition Algorithm
For each event in the process being manipulated,
1. if event writes version into variable , then the preversion, i.e. the version number of before this event being executed, must be 1. In other words, we have a transition from the state where evnt = with 1 to where evnt
= if the version number of is 1 in the state where evnt = . In this case we also modify the version number of from 1 to .
2. if event reads variable of version , then the preversion must be , i.e. we have a transition from the state where evnt = , with 1 to where evnt = if the version number of is in the state where evnt = . Note that the version number remains unchanged after this event.
3. the version number of event must be also less than or equal to all preversions of all other processes, according to the lastly executed event of each process.
Since the lastly executed events in other processes remains unchanged, the value of variable evnt keeps the same in each of other process after the transition. The version number of variable is, however, changed if the event is a write event on . Hence the must be less than or equal to the preversion of all other process to reserve the transition in other processes. If the version number of variable in event is greater than the perversion of some processes, event must wait until those processes are executed; otherwise those processes will never proceed anymore. This is the reason for the 3rd constraint, and thus constitutes the TRANS section in process modules..
The state variable prc indicates which process was running just before that state.
Hence after the module representing process 0 is executed, the value of prc must be
modified to 0. Note that prc, aVer, bVer are shared variables in each state and are declared and initialized in the main module. The main module is the one evaluated by the interpreter. Thus the modules for the processes are also instantiated in the VAR section of main module. Part of code for main module in this example is
MODULE main
The keyword process is used to compose the modules asynchronously.
Since this SYN-sequence has two variables a and b, we ought to declare a and b in NuSMV input file. However, if we declare both variables for the value and version number for each variable, we will double the state space. Since each version of a variable is mapped into exactly one value, we can use the define of NuSMV to assign the values of variables. The identifiers defined in the define section are similar to macros.
Using define to represent the values of the variables can avoid the enlargement of state space.
Progress Constraints
So far we still have to add some progress constraints for both stateful (general) and stateless model. This is done by adding a TRANS section in main module. Now let’s see the TRANS section for the given example:
TRANS
( next(p0.evnt) = p0.evnt & next(p1.evnt) = p1.evnt -> p0.evnt = 4 & p1.evnt = 4 ) & (next(p0.evnt) = 4
-> (p1.evnt = 3 | p1.evnt = 4)) & (next(p1.evnt) = 4
-> (p0.evnt = 3 | p0.evnt = 4))
NuSMV TRANS, as well as ASSIGN, is a type of constraint. All transitions must follow all constraints it involved. Thus the state variable evnt in each process module follows not only the ASSIGN constraints in that process module, but also the TRANS constraints in the main module. This is natural since we instantiate the process modules in the main module. But why should we add this TRANS constraint? We find the state variable evnt will remain unchanged if all conditions are false in the case analysis. This will lead to all processes idled in a state and is not allowed since we request all events of the SYN-sequence to be executed in exactly one state. The only exception is when all processes are terminated. Thus we add the first clause in the TRANS section to constrain that if all processes are idled, they must be all terminated. The remaining clauses further constrain the states from idle until all processes terminate. If these clauses are absent, we may have an execution path such that one process idled in the terminated event and all other processes idled in some non-terminated events.
Stateless Event Properties
Although the NuSMV model we have constructed so far is sufficient for verification, it is not convenient enough for programmer to use. This is because what we have constructed is only the skeleton of SYN-sequence with the pure stateful properties
involved. Our events are represented by process and event identifier. Again we use the define facility of NuSMV to supply the properties on events. Such properties are said to be stateless properties. The following DEFINE section is inserted into the main module of both general and stateless models:
CONSTANTS R, W, r, w, na, a, b;
val :=
case
vid = a & ver = 0 : 4;
vid = a & ver = 1 : 7;
vid = a & ver = 2 : 11;
vid = b & ver = 0 : 3;
1 : na;
The variables evnt, op, vid and ver define the information on an event just executed before a specific state. The val defines the value just accessed. We declared all constant symbols used in CONSTANTS section
Now we are equipped to express our specifications in LTL/CTL. We formulate the specifications that the value of variable remains 4 or 7 before variable being accessed and that event 1 of process 1 always happens before event 3 of process 0 as
LTLSPEC F((a=4 | a=7) & X F(vid=b)) LTLSPEC F(run=1 & p1.evnt=1
& X F(run=0 & p0.evnt=3))
in the main module. At last we can use NuSMV to verify whether the SYN-sequence given in Figure 3.3 satisfies our specifications.
Here we use the linear-time temporal logic (LTL) syntax of NuSMV, where , , , are presented as !, &, |, ->, respectively. Note that Boolean, CTL and some other specification formats can be used in NuSMV. Since the variables p0.evnt and p1.evnt keep the information that which event is lastly executed in process 0 and 1, respectively, run=0 & p0.evnt=3 can stand for event 3 of process 0 is executed just before that state.
These specifications are obviously false in the given SYN-sequence since event 3 of process 0 and event 1 of process 1 are parallel so any one of these events may happen before another one. Running NuSMV returns “false” and gives a counterexample for each of these specifications.