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

For the sake of simplicityassume in the following that the guard is satisfied.• Handshaking. If cap(c) = 0, then process Pi can transmit a value v over channel cby performingc!vi → ionly if another process Pj , say, “offers” a complementary receive action, i.e., canperformc?xj → j .Pi and Pj should thus be able to perform c!v (in Pi ) and c?x (in Pj ) simultaneously.Then, message passing can take place between Pi and Pj .

The effect of messagepassing corresponds to the (distributed) assignment x := v.Note that when handshaking is only used for synchronization purposes and not fordata transfer, the name of the channel as well as the value v are not of any relevance.• Asynchronous message passing. If cap(c) > 0, then process Pi can perform theconditional transitionc!vi → iif and only if channel c is not full, i.e., if less than cap(c) messages are stored in c.In this case, v is stored at the rear of the buffer c. Channels are thus considered asfirst-in, first-out buffers. Accordingly, Pj may performc?xj → jif and only if the buffer of c is not empty. In this case, the first element v of thebuffer is extracted and assigned to x (in an atomic manner).

This is summarized inTable 2.1.executable if . . .effectc!vc is not “full”Enqueue(c, v)c?xc is not emptyx := Front (c) ; Dequeue(c);Table 2.1: Enabledness and effect of communication actions if cap(c) > 0.Parallelism and Communication57channel dsynchronoussenderreceiverunreliable channel ctimerFigure 2.17: Schematic view of the alternating bit protocol.Channel systems are often used to model communication protocols. One of the mostelementary and well-known protocols is the alternating bit protocol.Example 2.32.Alternating Bit Protocol (ABP)Consider a system essentially consisting of a sender S and a receiver R that communicatewith each other over channels c and d, see Figure 2.17.

It is asssumed that both channelshave an unlimited buffer, i.e., cap(c) = cap(d) = ∞. Channel c is unreliable in thesense that data may get lost when being transmitted from the sender S to channel c.Once messages are stored in the buffer of channel c, they are neither corrupted nor lost.Channel d is assumed to be perfect. The goal is to design a communication protocol thatensures any distinct transmitted datum by S to be delivered to R. To ensure this in thepresence of possible message losses, sender S resorts to retransmissions.

Messages aretransmitted one by one, i.e., S starts sending a new message once the transmission of theprevious message has been successful. This is a simple flow control principle, known as“send-and-wait”.We abstract from the real activities of S and R and, instead, concentrate on a simplifiedrepresentation of the communication structure of the system. S sends the successivemessages m0 , m1 , . . . together with control bits b0 , b1 , .

. . over channel c to R. Transmittedmessages are thus pairs:m0 , 0, m1 , 1, m2 , 0, m3 , 1, . . .On receipt of m, b (along channel c), R sends an acknowledgment (ack) consisting ofthe control bit b just received. On receipt of ack b, S transmits a new message mwith control bit ¬b. If, however, S has to wait “too long” for the ack, it timeouts andretransmits m, b. The program graphs for S and R are sketched in Figure 2.18 and 2.19.For simplicity, the data that is transmitted is indicated by m instead of mi .58Modelling Concurrent Systemsc!m, 0snd msg(0)d?xst tmr(0)tmr on!wait(0)lostchk ack(0)x=1timeout?x=1:tmr off !x=0:tmr off !timeout?x=0chk ack(1)lostwait(1)tmr on!st tmr(1)d?xsnd msg(1)c!m, 1Figure 2.18: Program graph of ABP sender S.c?m, ywait(0)d!1snd ack(1)pr msg(0)snd ack(0)offtmr off ?y=1y=1y=0y=0pr msg(1)d!0 timeout!wait(1)tmr on?onc?m, yFigure 2.19: Program graph of (left) ABP receiver R and (right) Timer.Control bit b—also called the alternating bit—is thus used to distinguish retransmissionsof m from transmissions of subsequent (and previous) messages.

Due to the fact thatthe transmission of a new datum is initiated only when the last datum has been receivedcorrectly (and this is acked), a single bit is sufficient for this purpose and notions like, e.g.,sequence numbers, are not needed.The timeout mechanism of S is modeled by a Timer process. S activates this timer onsending a message (along c), and it stops the timer on receipt of an ack. When raisinga timeout, the timer signals to S that a retransmission should be initiated.

(Note thatdue to this way of modeling, so-called premature timeouts may occur, i.e., a timeout mayoccur whereas an ack is still on its way to S.) The communication between the timer andS is modeled by means of handshaking, i.e., by means of channels with capacity 0.Parallelism and Communication59The complete system can now be represented as the following channel system over Chan ={ c, d, tmr on, tmr off , timeout } and Var = { x, y, mi }:ABP = [S | Timer | R ] .The following definition formalizes the successive behavior of a channel system by meansof a transition system. The basic concept is similar to the mapping from a programgraph onto a transition system. Let CS = [PG1 | . .

. | PGn ] be a channel system over(Chan, Var). The (global) states of TS(CS) are tuples of the form1 , . . . , n , η, ξwhere i indicates the current location of component PGi , η keeps track of the currentvalues of the variables, and ξ records the current content of the various channels (as sequences). Formally, η ∈ Eval(Var) is an evaluation of the variables (as we have encounteredbefore), and ξ is a channel evaluation, i.e., a mapping from channel c ∈ Chan onto a sequence ξ(c) ∈ dom(c)∗ such that the length of the sequence cannot exceed the capacity of c,i.e., len(ξ(c)) cap(c) where len(·) denotes the length of a sequence.

Eval(Chan) denotesthe set of all channel evaluations. For initial states, the control components i ∈ Loc0,imust be initial and variable evaluation η must satisfy the initial condition g0 . In addition,every channel is initially assumed to be empty, denoted ε.Before providing the details of the semantics of a transition system, let us introduce somenotations. Channel evaluation ξ(c) = v1 v2 . .

. vk (where cap(c) k) denotes that v1 is atthe front of the buffer of c, v2 is the second element, etc., and vk is the element at the rearof c. len(ξ(c)) = k in this case. Let ξ[c := v1 , . . . , vk ] denote the channel evaluation wheresequence v1 , . . . , vk is assigned to c and all other channels are unaffected, i.e.,ξ(c )if c = cξ[c := v1 .

. . vk ](c ) =v1 . . . vk if c = c .The channel evaluation ξ0 maps any channel to the empty sequence, denoted ε, i.e., ξ0 (c) =ε for any channel c. Let len(ε) = 0. The set of actions of TS(CS) consists of actionsα ∈ Acti of component PGi and the distinguished symbol τ representing all communicationactions in which data is exchanged.Definition 2.33.Transition System Semantics of a Channel SystemLet CS = [P G1 | .

. . | P Gn ] be a channel system over (Chan, Var) withPGi = (Loci , Acti , Effecti , →i , Loc0,i , g0,i ) ,for 0 < i n.The transition system of CS, denoted TS(CS), is the tuple (S, Act, →, I, AP, L) where:60Modelling Concurrent Systems• S = (Loc1 × . . . × Locn ) × Eval(Var) × Eval(Chan),• Act = 0<in Acti { τ },• → is defined by the rules of Figure 2.20 (page 61),• I =1 , . .

. , n , η, ξ0 | ∀0 < i n. (i ∈ Loc0,i ∧ η |= g0,i ) ,• AP =0<in Loci Cond(Var),• L(1 , . . . , n , η, ξ) = { 1 , . . . , n } ∪ { g ∈ Cond(Var) | η |= g }.This definition is a formalization of the informal description of the interpretation of achannel system given before. Note that the labeling of the atomic propositions is similarto that for program graphs (see Definition 2.15). For the sake of simplicity, the abovedefinition does not allow for propositions on channels. This could be accommodated byallowing for conditions on channels such as, e.g., “the channel c is empty” or “the channelc is full”, and checking these conditions on the channel evaluation ξ in a state.Example 2.34.Alternating Bit Protocol (Revisited)Consider the alternating bit protocol that was modeled as a channel system in Example 2.32.

The underlying transition system TS(ABP ) has, despite various simplifyingassumptions, infinitely many states. This is, e.g., due to the fact that the timer may signal a timeout on each transmission of a datum by S resulting in infinitely many messagesin channel c.To clarify the functionality of the alternating bit protocol, consider two execution fragments represented by indicating the states of the various components (sender S, receiverR, the timer, and the contents of channels c and d).

The first execution fragment showsthe loss of a message. Here, R does not execute any action at all as it only acts if channelc contains at least one message:sender Ssnd msg(0)st tmr(0)wait (0)snd msg(0)...timeroffoffonoff...receiver Rwait (0)wait (0)wait (0)wait (0)...channel c channel d event∅∅∅∅loss of message∅∅∅∅timeout......Parallelism and Communication61• interleaving for α ∈ Acti :g:αi → i ∧ η |= gα1 , . .

. , i , . . . , n , η, ξ −−→ 1 , . . . , i , . . . , n , η , ξwhere η = Effect(α, η).• asynchronous message passing for c ∈ Chan, cap(c) > 0:– receive a value along channel c and assign it to variable x:g:c?xi → i ∧ η |= g ∧ len(ξ(c)) = k > 0 ∧ ξ(c) = v1 . . . vkτ1 , . . . , i , . . . , n , η, ξ −→1 , . . . , i , .

. . , n , η , ξ where η = η[x := v1 ] and ξ = ξ[c := v2 . . . vk ].– transmit value v ∈ dom(c) over channel c:g:c!vi → i ∧ η |= g ∧ len(ξ(c)) = k < cap(c) ∧ ξ(c) = v1 . . . vkτ1 , . . . , i , . . . , n , η, ξ −→1 , . . . , i , . . . , n , η, ξ where ξ = ξ[c := v1 v2 .