5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 63
Текст из файла (страница 63)
Explainhow the nested DFS can be modified to check directly whether TS |=wfair ♦a (where a ∈ AP),that is, without using the transformation TS |=wfair ♦a iff TS |= (wfair → ♦a).Exercise 5.23. Which of the following LTL formulae ϕi are representable by a deterministicBüchi automaton?ϕ1 = (a → ♦b), ϕ2 = ¬ϕ1 .Explain your answer.Exercise 5.24.
Check for the following LTL formula whether they are (i) satisfiable, and/or (ii)valid:(a) a ⇒ a(b) (a ∨ ♦ a) ⇒ ♦ a(c) a ⇒ ¬ ( ¬ a ∧ ¬ a)(d) ( a) U (♦ b) ⇒ (a U ♦ b)(e) ♦ b ⇒ (a U b)Practical ExercisesExercise 5.25. Consider an arbitrary, but finite, number of identical processes2, that execute inparallel. Each process consists of a noncritical part and a critical part, usually called the criticalsection. In this exercise we are concerned with the verification of a mutual exclusion protocol, thatis, a protocol that should ensure that at any moment of time at most one process (among the Nprocesses in our configuration) is in its critical section. There are many different mutual exclusionprotocols developed in the literature.
In this exercise we are concerned with Szymanski’s protocol[384]. Assume there are N processes for some fixed N > 0. There is a global variable, referred toas flag, which is an array of length N , such that flag[i] is a value between 0 and 4 (for 0 i < N ).The idea is that flag[i] indicates the status of process i. The protocol executed by process i looksas follows:l0: loop forever dobeginl1: Noncritical sectionl2: flag[i] := 1;2Only the identity of a process is unique.Exercises309l3: wait until (flag[0] < 3 and flag[1] < 3 and . .
. and flag[N-1] < 3)l4: flag[i] := 3;l5: if (flag[0] = 1 or flag[1] = 1 or . . . or flag[N-1] = 1)then beginl6: flag[i] := 2;l7: wait until (flag[0] = 4 or flag[1] = 4 or . . . or flag[N-1] = 4)endl8: flag[i] := 4;l9: wait until (flag[0] < 2 and flag[1] < 2 and . . . and flag[i-1] < 2)l10: Critical sectionl11: wait until (flag[i+1] ∈ { 0, 1, 4 }) and . . . and (flag[N-1] ∈ { 0, 1, 4 })l12: flag[i] := 0;end.Before doing any of the exercises listed below, try first to informally understand what the protocolis doing and why it could be correct in the sense that mutual exclusion is ensured.
If you areconvinced of the fact that the correctness of this protocol is not easy to see — otherwise pleaseinform me — then start with the following questions.1. Model Szymanski’s protocol in Promela. Assume that all tests on the global variable flag(such as the one in statement l3) are atomic. Look carefully at the indices of the variable flagused in the tests. Make the protocol description modular such that the number of processescan be changed easily.2. Check for several values of N (N 2) that the protocol indeed ensures mutual exclusion.Report your results for N equal to 4.3. The code that a process has to go through before reaching the critical section can be dividedinto several segments.
We refer to statement l4 as the doorway, to segments l5, l6, and l7, asthe waiting room and to segments l8 through l12 (which contains the critical section) as theinner sanctum. You are requested to check the following basic claims using assertions. Givefor each case the changes to your original Promela specification for Szymanski’s protocoland present the verification results. In case of negative results, simulate the counterexampleby means of guided simulation.(a) Whenever some process is in the inner sanctum, the doorway is locked, that is, noprocess is at location l4.(b) If a process i is at l10, l11 or l12, then it has the least index of all the processes in thewaiting room and the inner sanctum.(c) If some process is at l12, then all processes in the waiting room and in the inner sanctummust have flag value 4.Exercise 5.26.
We assume N processes in a ring topology, connected by unbounded queues.A process can only send messages in a clockwise manner. Initially, each process has a uniqueidentifier ident (which is assumed to be a natural number). A process can be either active or310Linear Temporal Logicrelaying. Initially a process is active. In Peterson’s leader election algorithm (1982) each processin the ring carries out the following task:active:d := ident;do foreverbegin/* start phase */send(d);receive(e);if e = ident then announce elected;if d > e then send(d) else send(e);receive(f );if f = ident then announce elected;if e max(d, f ) then d := e else goto relay;endrelay:do foreverbeginreceive(d);if d = ident then announce elected;send(d)endSolve the following questions concerning the leader election protocol:1.
Model Peterson’s leader election protocol in Promela (avoid invalid end states).2. Verify the following properties:(a) There is always at most one leader.(b) Eventually always a leader will be elected.(c) The elected leader will be the process with the highest number.(d) The maximum total amount of messages sent in order to elect a leader is at most2N 'log2 N ( + N .Exercise 5.27. This exercise deals with a simple fault-tolerant communication protocol in whichprocesses can fail.
A failed process is still able to communicate, i.e., it is able to send and receivemessages, but the content of its transmitted messages is unreliable. More precisely, a failed processcan send messages with arbitrary content. A failed process is therefore also called unreliable.We are given N reliable processes (i.e., processes that have not failed and that are working asexpected) and K unreliable processes, where N is larger than 3 · K and K is at least 0.
There is noway, a priori, to distinguish the reliable and the unreliable processes. All processes communicateExercises311by means of exchanging messages. Each process has a local variable, which initially has a value, 0or 1. The following informally described protocol is aimed to be followed by the reliable processes,such that at the end of round K+1 we have• eventually every reliable process has the same value in its local variable, and• if all reliable processes have the same initial value, then their final value is the same as theircommon initial value.The difficulty of this protocol is to establish these constraints in the presence of the K unreliableprocesses!Informal description of the protocol The following protocol is due to Berman and Garay[47].
Let the processes be numbered 1 through N +K. Processes communicate with each other in“rounds”. Each round consists of two phases of message transmissions: In round i, i > 0, in thefirst phase, every process sends its value to all processes (including itself); in the second phase,process i sends the majority value it received in the first phase (for majority to be well-defined weassume that N +K is odd) to all processes. If a process receives N , or more, instances of the samevalue in its first phase of the round, it sets its local variable to this value; otherwise, it sets itslocal variable to the value received (from process i) in the second phase of this round.1.
Model this protocol in Promela. Make the protocol description modular such that the number of reliable and unreliable processes can be changed easily. As the state space of yourprotocol model could be very large, instantiate your model with a single unreliable processand four reliable processes.First hint: One of the main causes for the large state space is the model for the unreliableprocess, so try to keep this model as simple as possible. This can be achieved by, for instance, assuming that an unreliable process can only transmit arbitrary 0 or 1 values (andnot any other value) and that a process always starts with a fixed initial value (and not witha randomly selected one). In addition, use atomic broadcast for message transmissions.Second hint: It might be convenient (though not necessary) to use a matrix of size (N +K) ·(N +K) of channels for the communication structure.
As Promela does not support multidimensional arrays, you could use the following construct (where M equals N +K):typedef Arraychan {chan ch[M] = [1] of {bit};}Arraychan A[M];/* M channels of size 1 *//* a matrix A of MxM channels of size 1 */Statement A[i].ch[j]!0 denotes an output of value 0 over the channel directed processfrom i to j.
Similarly, statement A[i].ch[j]?b denotes the receipt of a bit value stored invariable b via the channel directed from process i to j.2. Formalize the two constraints of the protocol in LTL and convert these into never claims.312Linear Temporal Logic3. Check the two temporal logic properties by Spin and hand in the verification output generated by Spin.4. Show that the requirement N > 3 · K is essential, by, for instance, changing the configuration of your system such that N 3 · K and checking that for this configuration thefirst aforementioned constraint is violated. Create the shortest counterexample (select theshortest trail in the advanced verification options) and perform a guided simulation of thisundesired scenario. Hand in the counterexample you found and give an explanation of it.Chapter 6Computation Tree LogicThis chapter introduces Computation Tree Logic (CTL), a prominent branching temporallogic for specifying system properties.
In particular, the syntax and semantics of CTLare presented, a comparison to Linear Temporal Logic (LTL) is provided, and the issueof fairness in CTL is treated. CTL model checking is explained in detail. First, the corerecursive algorithm is presented that is based on a bottom-up traversal of the parse tree ofthe formula at hand.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
