5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 16

. . vk v].• synchronous message passing over c ∈ Chan, cap(c) = 0:g1 :c?xg2 :c!vi → i ∧ η |= g1 ∧ η |= g2 ∧ j → j ∧ i = jτ1 , . . . , i , . . . , j , . . . , n , η, ξ −→1 , . . . , i , . . . , j , . . . , n , η , ξwhere η = η[x := v].Figure 2.20: Rules for the transition relation of a channel system.62Modelling Concurrent SystemsWhen the receiver R is in location wait(0) and receives a message, it anticipates receivinga message with either control bit 0 (as it expects) or with control bit 1, see left side ofFigure 2.19.

Symmetrically, in location wait(1) also the possibility is taken into accountto receive the (unexpected) ack with control bit 0. The following execution fragmentindicates why this unexpected possibility is essential to take into consideration. In anutshell, the execution fragment shows that it may happen that R receives m, 0, notifiesthis by means of sending an ack (with control bit 0), and switches to “mode 1”—waitingto receive a message with control bit 1. In the meanwhile, however, sender S has initiateda retransmission of m, 0 (as it timed out). On receipt of this (unexpected) message,receiver R should act accordingly and ignore the message.

This is exactly what happens.Note that if this possibility would not have been taken into consideration in the programgraph of R, the system would have come to a halt.sender Stimersnd msg(0) offst tmr (0)offreceiver Rwait (0)wait (0)channel c∅m, 0channel d∅∅wait (0)snd msg(0)st tmr (0)st tmr (0)onoffoffoffwait (0)wait (0)wait (0)pr msg(0)m, 0m, 0m, 0 m, 0m, 0∅∅∅∅st tmr (0)st tmr (0)offoffsnd ack(0) m, 0wait (1)m, 0st tmr (0)offpr msg(1)∅0st tmr (0)...off...wait (1)...∅...0...∅0eventmessage with bit 0transmittedtimeoutretransmissionreceiver readsfirst messagereceiver changesinto mode-1receiver readsretransmissionand ignores itWe conclude this example by pointing out a possible simplification of the program graph ofthe sender S.

Since the transmission of acks (over channel d) is reliable, it is unnecessary(but not wrong) for S to verify the control bit of the ack in location chk ack(·). If S is inlocation wait (0) and channel d is not empty, then the (first) message in d corresponds tothe expected ack 0, since R acknowledges each message m exactly once regardless of howmany times m is received. Therefore, the program graph of S could be simplified suchthat by the action sequence d?x ; timer off , it moves from location wait (0) to locationgen msg(1).

Location chk ack(0) may thus be omitted. By similar arguments, locationchk ack(1) may be omitted. If, however, channel d would be unreliable (like channel c),these locations are necessary.Parallelism and CommunicationRemark 2.35.63Open Channel SystemsThe rule for synchronous message passing is subject to the idea that there is a closedchannel system that does not communicate with the environment. To model open channelsystems, only the rule for handshaking has to be modified. If there is a channel c withcap(c) = 0 over which the channel system is communicating with the environment, therulesc!vi → ic!v1 , . . .

, i , . . . , n , η, ξ −−→ 1 , . . . , i , . . . , n , η, ξandc?xi → i ∧ v ∈ dom(c)c?x1 , . . . , i , . . . , n , η, ξ −−−→ 1 , . . . , i , . . . , n , η[x := v], ξhave to be used. The receipt of value v for variable x along channel c is modeled by meansof nondeterminism that is resolved by the environment.

That is to say, the environmentselects value v ∈ dom(c) in a purely nondeterministic way.2.2.5NanoPromelaThe concepts that have been discussed in the previous sections (program graphs, parallelcomposition, channel systems) provide the mathematical basis for modeling reactive systems. However, for building automated tools for verifying reactive systems, one aims atsimpler formalisms to specify the behavior of the system to be analyzed. On the one hand,such specification languages should be simple and easy to understand, such that nonexperts also are able to use them.

On the other hand, they should be expressive enough toformalize the stepwise behavior of the processes and their interactions. Furthermore, theyhave to be equipped with a formal semantics which renders the intuitive meaning of thelanguage commands in an unambiguous manner. In our case, the purpose of the formalsemantics is to assign to each program of the specification language a transition systemthat can serve as a basis for the automated analysis, e.g., simulation or model checkingagainst temporal logical specifications.In this section, we present the core features of the language Promela, the input languagefor the prominent model checker SPIN by Holzmann [209].

Promela is short for “processmetalanguage”. Promela programs P consist of a finite number of processes P1 , . . . , Pnto be executed concurrently. Promela supports communication over shared variables andmessage passing along either synchronous or buffered FIFO-channels. The formal semantics of a Promela-program can be provided by means of a channel system, which thencan be unfolded into a transition system, as explained in Section 2.2.4. The stepwisebehavior of the processes Pi is specified in Promela using a guarded command language64Modelling Concurrent Systems[130, 18] with several features of classical imperative programming languages (variable assignments, conditional and repetitive commands, sequential composition), communicationactions where processes may send and receive messages from the channels, and atomicregions that avoid undesired interleavings.

Guarded commands have already been used aslabels for the edges of program graphs and channel systems. They consist of a condition(guard) and an action. Promela does not use action names, but specifies the effect ofactions by statements of the guarded command language.Syntax of nanoPromela We now explain the syntax and semantics of a fragment ofPromela, called nanoPromela, which concentrates on the basic elements of Promela, butabstracts from details like variable declarations and skips several “advanced” conceptslike abstract data types (arrays, lists, etc.) or dynamic process creation. A nanoPromelaprogram consists of statements representing the stepwise behavior of the processes P1 , . .

. ,Pn together with a Boolean condition on the initial values of the program variables. Wewrite nanoPromela programs as:P = [P1 | . . . |Pn ].The main ingredients of the statements that formalize the stepwise behavior of the processes Pi are the atomic commands skip, variable assignments x := expr, communication actions c?x (reading a value for variable x from channel c) and c!expr (sending thecurrent value of an expression over channel c), conditional commands (if-then-else) and(while)loops.

Instead of the standard if-then-else constructs or whileloops, nanoPromelasupports nondeterministic choices and allows specifying a finite number of guarded commands in conditional and repetitive commands.Variables, Expressions and Boolean Expressions The variables in a nanoPromelaprogram P may be typed (integer, Boolean, char, real, etc.) and either global or local tosome process of Pi . Similarly, data domains have to be specified for the channels and theyhave to be declared to be synchronous or fifo-channels of a predefined capacity. We skipthe details of variable and channel declarations, as they are irrelevant for the purposesof this chapter.

As local variables can be renamed in case they occur in more than oneprocess or as the name of a global variable, we may treat all variables as global variables.Thus, we assume that Var is a set of variables occurring in P and that for any a variablename x the domain (type) of x is given as the set dom(x). Furthermore, in the declarationpart of a Promela program, the type of a channel is specified. We simply write here dom(c)for the type (domain) of channel c and cap(c) for its capacity. In addition, we assumethat the variable declaration of program P contains a Boolean expression that specifiesthe legal initial values for the variables x ∈ Var.Parallelism and Communication65stmt ::= skip | x := expr | c?x | c!expr |stmt1 ; stmt2 | atomic{assignments} |if:: g1 ⇒ stmt1 . .

. :: gn ⇒ stmtn fi|do :: g1 ⇒ stmt1 . . . :: gn ⇒ stmtn doFigure 2.21: Syntax of nanoPromela-statements.The intuitive meaning of an assignment x := expr is obvious: variable x is assigned thevalue of the expression expr given the current variable evaluation. The precise syntaxof the expressions and Boolean expressions is not of importance here.

We may assumethat the expressions used in assignments for variable x are built by constants in dom(x),variables y of the same type as x (or a subtype of x), and operators on dom(x), such asBoolean connectives ∧, ∨, ¬, etc. for dom(x) = { 0, 1 } and arithmetic operators +, ∗,etc. for dom(x) = R.3 The guards are Boolean expressions that impose conditions on thevalues of the variables, i.e., we treat the guards as elements of Cond(Var).Statements The syntax of the statements that specify the behavior of the nanoPromelaprocesses is shown in Figure 2.21 on page 65.Here, x is a variable in Var, expr anexpression, and c is a channel of arbitrary capacity. Type consistency of the variable xand the expression expr is required in assignments x := expr. Similarly, for the messagepassing actions c?x and c!expr we require that dom(c) ⊆ dom(x) and that the type of exprcorresponds to the domain of c.

The gi ’s in if–fi- and do–od-statements are guards. Asmentioned above, we assume that gi ∈ Cond(Var). The body assignments of an atomicregion is a nonempty sequential composition of assignments, i.e., assignments has the formx1 := expr1 ; x2 := expr2 ; . . . ; xm := exprmwhere m 1, x1 , . . .

, xm are variables and expr1 , . . . , exprm expressions such that the typesof xi and expri are compatible.Intuitive Meaning of the Commands Before presenting the formal semantics, letus give some informal explanations on the meaning of the commands. skip stands fora process that terminates in one step, without affecting the values of the variables orcontents of the channels. The meaning of assignments is obvious. stmt1 ; stmt2 denotessequential composition, i.e., stmt1 is executed first and after its termination stmt2 is executed. The concept of atomic regions is realized in nanoPromela by statements of the3For simplicity, the operators are supposed to be total.