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

The complete systemTSArb = (TS1 ||| TS2 ) Arbiterguarantees mutual exclusion since there are no states of TSArb where both P1 and P2 arein their critical section (see bottom part of Figure 2.12). Note that in the initial state ofTS1 ||| TS2 , the Arbiter determines which process will enter the critical section next.Example 2.29.Booking SystemConsider a (strongly simplified) booking system at a cashier of a supermarket. The systemconsists of three processes: the bar code reader BCR, the actual booking program BP,and the printer Printer. The bar code reader reads a bar code and communicates thedata of the just scanned product to the booking program. On receiving such data, thebooking program transmits the price of the article to the printer that prints the article Idtogether with the price on the receipt. The interactions between the bar code reader andthe booking program, and between the booking program and the printer is performed byhandshaking.

Each process consist of just two states, named 0 and 1 (see Figure 2.13 forthe transitions systems of BCR, BP, and Printer).The complete system is given by:BCR BP Printer.The transition system of the overall system is depicted in Figure 2.14 on page 52. Theinitial global state of this system is 0, 0, 0, or in short, 000. In global state 010, e.g., theParallelism and CommunicationT1T2 :51Arbiter:noncrit1 noncrit2unlockcrit1 noncrit2noncrit1 crit2releaserequestlockcrit1 crit2T1T2Arbiter :noncrit1 noncrit2 unlockreleasereleaserequest requestcrit1 noncrit2 locknoncrit1 crit2 lockFigure 2.12: Mutual exclusion using handshaking with arbiter process.nondeterminism stands for the concurrent execution of the actions scanning the bar codeand the synchronous transfer of the price to the printer.Example 2.30.Railroad CrossingFor a railroad crossing a control system needs to be developed that on receipt of a signalindicating that a train is approaching closes the gates, and only opens these gates after thetrain has sent a signal indicating that it crossed the road.

The requirement that should bemet by the control system is that the gates are always closed when the train is crossing theroad. The complete system consists of the three components Train, Gate, and Controller:Train Gate Controller.Figure 2.15 depicts the transition systems of these components from left (modeling theTrain) to right (modeling the Gate).

For simplicity, it is assumed that all trains passthe relevant track section in the same direction—from left to right. The states of thetransition system for the Train have the following intuitive meaning: in state far the trainis not close to the crossing, in state near it is approaching the crossing and has just sent asignal to notify this, and in state in it is at the crossing. The states of the Gate have theobvious interpretation.

The state changes of the Controller stand for handshaking with52Modelling Concurrent Systems00scanstoreprt cmd10storeprint1prt cmd1Figure 2.13: The components of the book keeping example.101printstoreprt cmdscan100 scan 000001print110print111 scan 011scanprt cmdstoreprint010Figure 2.14: Transition system representation of the booking system.the trains (via the actions approach and exit) and the Gate (via the actions lower andraise via which the Controller causes the gate to close or to open, respectively).Figure 2.16 (above) illustrates the transition system of the overall system. A closer inspection of this transition system reveals that the system suffers from a design flaw.

Thiscan be seen from the following initial execution fragment:approachenter−−−−→ near , 1, up −−−−→ in, 1, upfar , 0, up −−in which the gate is about to close, while the train is (already) at the crossing. Thenondeterminism in global state near , 1, up stands for concurrency: the train approachesthe crossing, while the gate is being closed. In fact, the basic concept of the designis correct if and only if closing the gate does not take more time than the train needsto get to the crossing once it signals—“I am approaching”.

Such real-time constraintscannot be formulated by the concepts introduced so far. The interleaving representationfor parallel systems is completely time-abstract. In Chapter 9, concepts and techniqueswill be introduced to specify and verify such real-time aspects.Parallelism and Communicationfarapproachexitnearenter53upapproach 0 raise13raiselowerinlower 2 exitdownTrainControllerGateFigure 2.15: The components of the railroad crossing.2.2.4Channel SystemsThis section introduces channel systems, parallel systems where processes communicatevia so-called channels, i.e., first-in, first-out buffers that may contain messages. We consider channel systems that are closed. That is to say, processes may communicate withother processes in the system (via channels), but not with processes outside the system.Channel systems are popular for describing communication protocols and form the basisof Promela, the input language of the Spin model checker.Intuitively, a channel system consists of n (data-dependent) processes P1 through Pn .Each Pi is specified by a program graph PGi which is extended with communicationactions.

Transitions of these program graphs are either the usual conditional transitions(labeled with guards and actions) as before, or one of the communication actions withtheir respective intuitive meaning:c!vc?xtransmit the value v along channel c,receive a message via channel c and assign it to variable x.When considering channel c as buffer, the communication action c!v puts value v (at therear of) the buffer whereas c?x retrieves an element from (the front of) the buffer whileassigning it to x. It is assumed implicitly that variable x is of the right type, i.e., it has atype that is compatible to that of the messages that are put into channel c. LetComm =c!v, c?x | c ∈ Chan, v ∈ dom(c), x ∈ Var with dom(x) ⊇ dom(c)denote the set of communication actions where Chan is a finite set of channels with typicalelement c.54Modelling Concurrent Systemsfar, 0, upapproachnear, 1, uplowerenternear, 2, down lowerenterraisein, 1, upexitfar, 1, upin, 2, downexitapproachapproachlowerfar, 2, downfar, 3, downapproachexitnear, 3, downenterraisenear, 0, upin, 3, downexitexitenterin, 0, upFigure 2.16: Transition system for the railroad crossing.Parallelism and Communication55A channel c has a (finite or infinite) capacity indicating the maximum number of messagesit can store, and a type (or domain) specifying the type of messages that can be transmittedover c.

Each channel c has a capacity cap(c) ∈ IN ∪ { ∞ }, and a domain dom(c). For achannel c that can only transfer bits, dom(c) = { 0, 1 }. If complete texts (of maximumlength of 200, say) need to be transmitted over channel c, then another type of channelhas to be used such that dom(c) = Σ200 , where Σ is the alphabet that forms the basis ofthe texts, e.g., Σ is the set of all letters and special characters used in German texts.The capacity of a channel defines the size of the corresponding buffer, i.e., the number ofmessages not yet read that can be stored in the buffer. When cap(c) ∈ IN, c is a channelwith finite capacity; cap(c) = ∞ indicates that c has an infinite capacity.

Note that thespecial case cap(c) = 0 is permitted. In this case, channel c has no buffer. Communicationvia such a channel c corresponds to handshaking (simultaneous transmission and receipt,i.e., synchronous message passing) plus the exchange of some data. When cap(c) > 0,there is a “delay” between the transmission and the receipt of a message, i.e., sending andreading of the same message take place at different moments. This is called asynchronousmessage passing.

Sending and reading a message from a channel with a nonzero capacitycan never appear simultaneously. By means of channel systems, both synchronous andasynchronous message passing can thus be modeled.Definition 2.31.Channel SystemA program graph over (Var, Chan) is a tuplePG = (Loc, Act, Effect, →, Loc0 , g0 )according to Definition 2.13 (page 32) with the only difference that→⊆Loc × (Cond(Var) × (Act ∪ Comm) × Loc.A channel system CS over (Var, Chan) consists of program graphs PGi over (Vari , Chan)(for 1 i n) with Var = 1in Vari .

We denoteCS = [PG1 | . . . | PGn ] .The transition relation → of a program graph over (Var, Chan) consists of two typesg:αof conditional transitions. As before, conditional transitions → are labeled withguards and actions. These conditional transitions can happen whenever the guard holds.Alternatively, conditional transitions may be labeled with communication actions. Thisg:c!vg:c?xyields conditional transitions of type → (for sending v along c) and → (forreceiving a message along c). When can such conditional transitions happen? Stated56Modelling Concurrent Systemsdifferently, when are these conditional transitions executable? This depends on the currentvariable evaluation and the capacity and content of the channel c.