5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 17
Текст из файла (страница 17)
For operators that require special arguments(e.g., division requires a nonzero second argument) we assume that the corresponding domain contains aspecial element with the meaning of “undefined”.66Modelling Concurrent Systemsform atomic{stmt}. The effect of atomic regions is that the execution of stmt is treatedas an atomic step that cannot be interleaved with the activities of other processes. As aside effect atomic regions can also serve as a compactification technique that compressesthe state space by ignoring the intermediate configurations that are passed during theexecutions of the commands inside an atomic region. The assumption that the body of anatomic region consists of a sequence of assignments will simplify the inference rules givenbelow.Statements build by if–fi or do–od are generalizations of standard if-then-else commandsand whileloops.
Let us first explain the intuitive meaning of conditional commands. Thestatementif :: g1 ⇒ stmt1 . . . :: gn ⇒ stmtn fistands for a nondeterministic choice between the statements stmti for which the guard giis satisfied in the current state, i.e., gi holds for the current valuation of the variables. Weassume a test-and-set semantics where the evaluation of the guards, the choice betweenthe enabled guarded commands and the execution of the first atomic step of the selectedstatement, are performed as an atomic unit that cannot be interleaved with the actions ofconcurrent processes. If none of the guards g1 , .
. . , gn is fulfilled in the current state, thenthe if–fi–command blocks. Blocking has to be seen in the context of the other processesthat run in parallel and that might abolish the blocking by changing the values of sharedvariables such that one or more of the guards may eventually evaluate to true. For instance,the process given by the statementif :: y > 0 ⇒ x := 42 fiin a state where y has the value 0 waits until another process assigns a nonzero value toy. Standard if-then-else commands, say “if g then stmt1 else stmt2 fi”, of imperativeprogramming languages can be obtained by:if :: g ⇒ stmt1 :: ¬g ⇒ stmt2 fi,while statements “if g then stmt1 fi” without an else option are modeled by:if :: g ⇒ stmt1 :: ¬g ⇒ skip fi.In a similar way, the do–od-command generalizes whileloops.
These specify the repetitionof the body, as long as one of the guards is fulfilled. That is, statements of the form:do :: g1 ⇒ stmt1 . . . :: gn ⇒ stmtn odstand for the iterative execution of the nondeterministic choice among the guarded commands gi ⇒ stmti where guard gi holds in the current configuration. Unlike conditionalcommands, do–od-loops do not block in a state if all guards are violated.
Instead, ifParallelism and Communication67g1 , . . . , gn do not hold in the current state, then the whileloop is aborted. In fact, a singleguarded loop do :: g ⇒ stmt od has the same effect as an ordinary whileloop “whileg do stmt od” with body stmt and termination condition ¬g. (As opposed to Promela,loops are not terminated by the special command “break”.)Example 2.36.Peterson’s Mutual Exclusion AlgorithmPeterson’s mutual exclusion algorithm for two processes (see Example 2.25 on page 45)can be specified in nanoPromela as follows.
We deal with two Boolean variables b1 andb2 and the variable x with domain dom(x) = {1, 2} and two Boolean variables crit1 andcrit2 . The activities of the processes inside their noncritical sections are modeled by theaction skip. For the critical section, we use the assignment criti := true. Initially, wehave b1 = b2 = crit1 = crit2 = false, while x is arbitrary. Then the nanoPromela-code ofprocess P1 is given by the statementdo :: true ⇒ skip;atomic{b1 := true; x := 2};if :: (x = 1) ∨ ¬b2 ⇒ crit1 := true fiatomic{crit1 := false; b1 := false}odThe statement for modeling the second process is similar.
The infinite repetition of thethree phases “noncritical section”, “waiting phase” and “critical section” is modeled by thedo–od-loop with the trivial guard true. The request action corresponds to the statementatomic{b1 := true; x := 2} and the release action to the statement atomic{crit1 :=false; b1 := false}. The waiting phase where process P1 has to await until x = 1 orb2 = false is modeled by the if–fi-command.The use of atomic regions is not necessary, but serves here as a compactification technique.As we mentioned in Example 2.25, the request action can also be split into the twoassignments b1 := true and x := 2. As long as both assignments are inside an atomicregion the order of the assignments b1 := true and x := 2 is irrelevant. If, however, wedrop the atomic region, then we have to use the order b1 := true; x := 2, as otherwise themutual exclusion property cannot be ensured.
That is, the processdo :: true ⇒ skip;x := 2;b1 := true;if :: (x = 1) ∨ ¬b2 ⇒ crit1 := true fiatomic{crit1 := false; b1 := false}odfor P1 together with the symmetric protocol for P2 constitutes a nanoPromela programwhere the mutual exclusion property “never crit1 = crit2 = true” cannot be guaranteed.68Example 2.37.Modelling Concurrent SystemsVending MachineIn the above example there are no nondeterministic choices caused by a conditional orrepetitive command. For an example where nondeterminism arises through simultaneouslyenabled guarded commands of a loop, consider the beverage vending machine of Example2.14 (page 33).
The following nanoPromela program describes its behavior:do :: true ⇒skip;if:: nsoda > 0 ⇒ nsoda := nsoda − 1:: nbeer > 0 ⇒ nbeer := nbeer − 1:: nsoda = nbeer = 0 ⇒ skipfi:: true ⇒ atomic{nbeer := max; nsoda := max}odIn the starting location, there are two options that are both enabled. The first is theinsertion of a coin by the user, modeled by the command skip.
The first two options ofthe if–fi-command represent the cases where the user selects soda or beer, provided somebottles of soda and beer, respectively, are left. The third guarded command in the if–fisubstatement applies to the case where neither soda nor beer is available anymore and themachine automatically returns to the initial state. The second alternative that is enabledin the starting location is the refill action whose effect is specified by the atomic regionwhere the variables nbeer and nsoda are reset to max.Semantics The operational semantics of a nanoPromela-statement with variables andchannels from (Var, Chan) is given by a program graph over (Var, Chan).The program graphs PG1 , .
. ., PGn for the processes P1 , . . . , Pn of a nanoPromela program P =[P1 | . . . |Pn ] constitute a channel system over (Var, Chan). The transition system semantics for channel systems (Definition 2.31 on page 55) then yields a transition system TS(P)that formalizes the stepwise behavior of P.The program graph associated with a nanoPromela-statement stmt formalizes the controlflow when executing stmt.
That is, the substatements play the role of the locations. Formodeling termination, a special location exit is used. Roughly speaking, any guardedcommand g ⇒ stmt corresponds to an edge with the label g : α where α stands for thefirst action of stmt. For example, for the statementcond cmd = if :: x > 1 ⇒ y := x + y:: true⇒ x := 0; y := xfiParallelism and Communication69from cond cmd – viewed as a location of a program graph – there are two edges: one withthe guard x > 1 and action y := x + y leading to exit, and one with the guard true andaction x := 0 yielding the location for the statement y := x. Since y := x is deterministicthere is a single edge with guard true, action y := x leading to location exit.As another example, consider the statementloop = do :: x > 1 ⇒ y := x + y:: y < x ⇒ x := 0; y := xodHere, the repetition semantics of the do–od-loop is modeled by returning the control tostmt whenever the body of the selected alternative has been executed.
Thus, from locationloop there are three outgoing edges, see Figure 2.22 on page 69. One is labeled with theguard x > 1 and action y := x + y and leads back to location loop. The second edge hasthe guard y < x and action x := 0 and leads to the statement y := x ; loop. The thirdedge covers the case where the loop terminates. It has the guard ¬(x > 1) ∧ ¬(y < x) andan action without any effect on the variables and leads to location exit.true : y := xy := x ; looploop¬(x > 1) ∧ ¬(y < x)exity < x : x := 0x > 1 : y := x+yFigure 2.22: Program graph for a loopThe goal is now to formalize the ideas sketched above. We start with a formal definition ofsubstatements of stmt. Intuitively, these are the potential locations of intermediate statesduring the execution of stmt.Notation 2.38.SubstatementThe set of substatements of a nanoPromela-statement stmt is recursively defined.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
