5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 89
Текст из файла (страница 89)
and their vertical positionsASSIGN -- the initial horizontal and vertical positions of all tilesinit(h[0])init(h[1])init(h[2])init(h[3])init(h[4])init(h[5])init(h[6])init(h[7])init(h[8]):=:=:=:=:=:=:=:=:=1;2;3;1;2;3;1;2;3;init(v[0])init(v[1])init(v[2])init(v[3])init(v[4])init(v[5])init(v[6])init(v[7])init(v[8]):=:=:=:=:=:=:=:=:=3;3;3;2;2;2;1;1;1;ASSIGN-- determine the next positions of the blank tilenext(h[0]) :=case-- horizontal position of the blank tile1 : h[0];-- one position right-- one position left-- keep the same horizontal positionesac;next(v[0]) :=case-- vertical position of the blank tile1 : v[0];-- one position down-- one position up-- keep the same vertical positionesac;-- determine the next positions of all non-blank tilesnext(h[1]) :=caseesac;-- horizontal position of tile 1Exercises445next(v[1]) :=case-- vertical position of tile 1esac;-- and similar for all remaining tilesA possible way to proceed is as follows:(i) First, consider the possible moves of the blank tile (i.e., the blank space).
Notice thatthe blank space cannot be moved to the left in all positions. The same applies to movesupward, downward and to the right.(ii) Then try to find the possible moves of tile [1]. The code for tiles [2] through [8] areobtained by simply copying the code for tile [1] while replacing all references to [1]with references of the appropriate tile number.(iii) Test the possible moves by running a simulation.(b) Define an atomic proposition goal that describes the desired goal configuration of the puzzle.Add this definition to your NuSMV specification by incorporating the following line(s) inyour NuSMV model:DEFINE goal :=..............
;where the dotted lines contain your description of the goal configuration.(c) Find a solution to the puzzle by imposing the appropriate CTL formula to the NuSMVspecification, and running the model checker on this formula.This exercise has been taken from [95].Exercise 6.33. Consider the mutual exclusion algorithm by the Dutch mathematician Dekker.There are two processes P1 and P2 , two Boolean-valued variables b1 and b2 whose initial valuesare false, and a variable k which may take the values 1 and 2 and whose initial value is arbitrary.The ith process (i=1, 2) may be described as follows, where j is the index of the other process:while true dobegin bi := true;while bj doif k = j then beginbi := false;while k = j do skip;bi := trueend; critical section ;k := j;bi := falseend446Computation Tree LogicQuestions:(a) Model Dekker’s algorithm in NuSMV.(b) Verify whether this algorithm satisfies the following properties:(c) Mutual exclusion: two processes cannot be in their critical section at the same time.(d) Absence of individual starvation: if a process wants to enter its critical section, it is eventuallyable to do so.(Hint: use the FAIRNESS running statement in your NuSMV specification for proving the latterproperty in order to prohibit unfair executions that might trivially violate these requirements.)Exercise 6.34.
In the original mutual exclusion protocol by Dijkstra in 1965 (another Dutchmathematician), it is assumed that there are n 2 processes, and global variables b, c : array [1 . . . n]of Boolean and an integer k. Initially all elements of b and of c have the value true and the valueof k belongs to 1, 2, .
. . , n. The ith process may be represented as follows:var j : integer;while true dobegin b[i] := false;Li : if k = i then begin c[i] := true;if b[k] then k := i;goto Liend;else begin c[i] := false;for j := 1 to n doif (j = i ∧ ¬ (c[j])) then goto Liend critical section ;c[i] := true;b[i] := trueendQuestions:(a) Model this algorithm in NuSMV.(b) Check the mutual exclusion property (at most one process can be in its critical section atany point in time) in two different ways: by means of a CTL formula using SPEC and byusing invariants. Try to check this property for n=2 through n=5 by increasing the numberof processes gradually and compare the sizes of the state spaces and the runtime needed forthe two ways of verifying the mutual exclusion property.(c) Check the absence of individual starvation property: if a process wants to enter its criticalsection, it is eventually able to do so.Exercises447Exercise 6.35.
In order to find a fair solution for N processes, Peterson proposed in 1981 thefollowing protocol. Let Q[1 . . . N ] (Q for queue) and T [1 . . . N ] (T for turn), be two shared arrayswhich are initially 0 and 1, respectively. The variables i and j are local to the process with icontaining the process number. The code of process i is as follows:while true dofor j := 1 to N − 1 dobeginQ[i] := j;T [j] := i;wait until (T [j] = i ∨ (forall k = i.
Q[k] < j))end; critical section ;Q[i] := 0endQuestions:(a) Model Peterson’s algorithm in NuSMV.(b) Verify whether this algorithm satisfies the following properties:(i) Mutual exclusion.(ii) Absence of individual starvation.Chapter 7Equivalences and AbstractionTransition systems can model a piece of software or hardware at various abstraction levels.The lower the abstraction level, the more implementation details are present. At highabstraction levels, such details are deliberately left unspecified. Binary relations betweenstates (henceforth implementation relations) are useful to relate or to compare transitionsystems, possibly at different abstraction levels. When two models are related, one modelis said to be refined by the other, or, reversely, the second is said to be an abstraction ofthe first.
If the implementation relation is an equivalence, then it identifies all transitionsystems that cannot be distinguished; such models fulfill the same observable propertiesat the relevant abstraction level.Implementation relations are predominantly used for comparing two models of the samesystem. Given a transition system TS that acts as an abstract system specification, anda more detailed system model TS , implementation relations allow checking whether TSis a correct implementation (or: refinement) of TS.
Alternatively, for system analysispurposes, implementation relations provide ample means to abstract from certain systemdetails, preferably details that are irrelevant for the analysis of the property, ϕ say, athand. In this way, a transition system TS comprising very many, maybe even infinitelymany, states can be abstracted by a smaller model TS.
Provided the abstraction preservesthe property to be checked, the analysis of the (hopefully small) abstract model TS sufficesto decide the satisfaction of the properties in TS . Formally, from TS |= ϕ we may safelyconclude TS |= ϕ.This chapter will introduce several implementation relations, ranging from very strict ones(“strong” relations) that require transition systems to mutually mimic each transition, tomore liberal ones (“weak” relations) in which this is only required for certain transitions.449450Equivalences and AbstractionIn fact, in this monograph we have already encountered implementation relations thatwere aimed at comparing transition systems by considering their linear-time behavior,i.e., (finite or infinite) traces.
Examples of such relations are trace inclusion and traceequivalence. Linear-time properties or LTL formulae are preserved by trace relationsbased on infinite traces; for trace-equivalent TS and TS and linear-time property P , wehave TS |= P whenever TS |= P . A similar result is obtained when replacing P by anLTL formula.Besides the introduction of a weak variant of trace equivalence, the goal of this chapter isprimarily to study relations that respect the branching-time behavior. Classical representatives of such relations are bisimulation equivalences and simulation preorder relations.Whereas bisimulation relates states that mutually mimic all individual transitions, simulation requires that one state can mimic all stepwise behavior of the other, but not thereverse.
Weak variants of these relations only require this for certain (“observable”) transitions, and not for other (“silent”) transitions. This chapter will formally define strong andweak variants of (bi)simulation, and will treat their relationship to trace-based relations.The preservation of CTL and CTL∗ formulae is shown; for bisimulation the truth valueof all such formulae is preserved, while for simulation this applies to a (large) fragmentthereof.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
