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

Forexample, a proposition like(x 5) ∧ (y is even) ∧ ( ∈ { 1, 2 })34Modelling Concurrent Systemscan be formulated with x, y being integer variables and with locations being naturals.The labeling of states is such that , v is labeled with and with all conditions (overg:α−→ Var) that hold in η. The transition relation is determined as follows. Whenever −−is a conditional transition in the program graph, and the guard g holds in the currentevaluation η, then there is a transition from state , η to state , Effect(α, η). Notethat the transition is not guarded.

Formally:Definition 2.15.Transition System Semantics of a Program GraphThe transition system TS(PG) of program graphPG = (Loc, Act, Effect, →, Loc0 , g0 )over set Var of variables is the tuple (S, Act, −→, I, AP, L) where• S = Loc × Eval(Var)• −→ ⊆ S × Act × S is defined by the following rule (see remark below):g:α → ∧ η |= gα, η −−→ , Effect(α, η)• I = {, η | ∈ Loc0 , η |= g0 }• AP = Loc ∪ Cond(Var)• L(, η) = {} ∪ {g ∈ Cond(Var) | η |= g}.The definition of TS(PG) determines a very large set of propositions AP. But generally,only a small part of AP is necessary to formulate the relevant system properties.

In thefollowing, we exploit the degrees of freedom in choosing the set of propositions of TS(PG)and only use the atomic propositions needed in the context at hand.Remark 2.16.Structured Operational SemanticsIn Definition 2.15, the transition relation is defined using the so-called SOS-notation(Structured Operational Semantics).

This notation will be frequently used in the remainder of this monograph. The notationpremiseconclusionParallelism and Communication35should be read as follows. If the proposition above the “solid line” (i.e., the premise) holds,then the proposition under the fraction bar (i.e., the conclusion) holds as well. Such “if. . ., then . . .” propositions are also called inference rules or simply rules. If the premise isa tautology, it may be omitted (as well as the “solid line”). In the latter case, the rule isalso called an axiom.Phrases like “The relation → is defined by the following (axioms and) rules” have themeaning of an inductive definition where the relation → is defined as the smallest relationsatisfying the indicated axioms and rules.2.2Parallelism and CommunicationIn the previous section, we have introduced the notion of transition systems and haveshown how sequential hardware circuits and data-dependent systems (like simple sequential computer programs) can be effectively modeled as transition systems.

In reality,however, most hard- and software systems are not sequential but parallel in nature. Thissection describes several mechanisms to provide operational models for parallel systemsby means of transition systems. These mechanisms range from simple mechanisms whereno communication between the participating transitions systems takes place, to more advanced (and realistic) schemes in which messages can be transferred, either synchronously(i.e., by means of “handshaking”) or asynchronously (i.e., by buffers with a positive capacity). Let us assume that the operational (stepwise) behavior of the processes that runin parallel are given by transition systems TS1 , . .

. , TSn . The goal is to define an operator, such that:TS = TS1 TS2 . . . TSnis a transition system that specifies the behavior of the parallel composition of transitionsystems TS1 through TSn . Here, it is assumed that is a commutative and associativeoperator. The nature of the operator will, of course, depend on the kind of communication that is supported. We will for instance see that some notions of parallel compositiondo not yield an associative operator. In the remainder of this section, several variants of will be considered and illustrated by means of examples. Note that the above schememay be repeated for TSi , i.e., TSi may again be a transition system that is composed ofseveral transition systems:TSi = TSi,1 TSi,1 . .

. TSi,ni .36Modelling Concurrent SystemsBy using parallel composition in this hierarchical way, complex systems can be describedin a rather structured way.2.2.1Concurrency and InterleavingA widely adopted paradigm for parallel systems is that of interleaving. In this model,one abstracts from the fact that a system is actually composed of a set of (partly) independent components. That is to say, the global system state – composed of the currentindividual states of the components – plays a key role in interleaving. Actions of anindependent component are merged (also called weaved), or “interleaved”, with actionsfrom other components. Thus, concurrency is represented by (pure) interleaving, that is,the nondeterministic choice between activities of the simultaneously acting processes (orcomponents).

This perspective is based on the view that only one processor is availableon which the actions of the processes are interlocked. The “one-processor view” is only amodeling concept and also applies if the processes run on different processors. Thereby,(at first) no assumptions are made about the order in which the different processes areexecuted. If there are, e.g., two nonterminating processes P and Q, say, acting completelyindependent of each other, thenPPPQ P Q P Q Q Q P ...P Q P P Q P P Q ...Q P P Q P P P Q ...are three possible sequences in which the steps (i.e., execution of actions) of P and Q canbe interlocked. (In Chapter 3, certain restrictions will be discussed to ensure that eachparticipating processor is treated in a somewhat “fair” manner.

In particular, executionsequences like P, P, P, . . ., where Q is completely ignored, are ruled out. Unless statedotherwise, we accept all possible interleavings, including the unfair ones.)The interleaving representation of concurrency is subject to the idea that there is a scheduler which interlocks the steps of concurrently executing processes according to an a prioriunknown strategy. This type of representation completely abstracts from the speed ofthe participating processes and thus models any possible realization by a single-processormachine or by several processors with arbitrary speeds.Example 2.17.Two Independent Traffic LightsConsider the transition systems of two traffic lights for nonintersecting (i.e., parallel)roads.

It is assumed that the traffic lights switch completely independent of each other.For example, the traffic lights may be controlled by pedestrians who would like to cross theroad. Each traffic light is modeled as a simple transition system with two states, one stateParallelism and Communication37TrLight1redgreenTrLight2redgreenTrLight1 ||| TrLight2red redred greengreen redgreen greenFigure 2.4: Example of interleaving operator for transition systems.modeling a red light, the other one modeling a green light (see upper part of Figure 2.4).The transition system of the parallel composition of both traffic lights is sketched at thebottom of Figure 2.4 where ||| denotes the interleaving operator. In principle, any formof interlocking of the “actions” of the two traffic lights is possible. For instance, in theinitial state where both traffic lights are red, there is a non-deterministic choice betweenwhich of the lights turns green.

Note that this nondeterminism is descriptive, and doesnot model a scheduling problem between the traffic lights (although it may seem so).An important justification for interleaving is the fact that the effect of concurrently executed, independent actions α and β, say, is identical to the effect when α and β aresuccessively executed in arbitrary order. This can symbolically be stated asEffect(α ||| β, η) = Effect((α ; β) + (β ; α), η)where the operator semicolon ; stands for sequential execution, + stands for nondeterministic choice, and ||| for the concurrent execution of independent activities. This fact canbe easily understood when the effect is considered from two independent value assignments38Modelling Concurrent Systemsxx + 1 ||| y := y − 2.

:= =α=βWhen initially x = 0 and y = 7, then x has the value 1 and y the value 5 after executing αand β, independent of whether the assignments occur concurrently (i.e., simultaneously)or in some arbitrary successive order. This is depicted in terms of transition systems asfollows:αx=1αy=7x=0|||β=x=0, y=7x=1, y=7βy=5βx=0, y=5x=1, y=5αNote that the independence of actions is crucial. For dependent actions, the order ofactions is typically essential: e.g., the final value of variable x in the parallel programx := x+1 ||| x := 2·x (with initial value x=0, say) depends on the order in which theassignments x := x+1 and x := 2·x take place.We are now in a position to formally define the interleaving (denoted ||| ) of transitionsystems. The transition system TS1 ||| TS2 represents a parallel system resulting fromthe weaving (or merging) of the actions of the components as described by TS1 andTS2 .

It is assumed that no communication and no contentions (on shared variables)occur at all. The (“global”) states of TS1 ||| TS2 are pairs s1 , s2 consisting of “local”states si of the components TSi . The outgoing transitions of the global state s1 , s2 consist of the outgoing transitions of s1 together with those of s2 . Accordingly, wheneverthe composed system is in state s1 , s2 , a nondeterministic choice is made between alloutgoing transitions of local state s1 and those of local state s2 .Definition 2.18.Interleaving of Transition SystemsLet TSi = (Si , Acti , →i , Ii , APi , Li ) i=1, 2, be two transition systems. The transitionsystem TS1 ||| TS2 is defined by:TS1 ||| TS2 = (S1 × S2 , Act1 ∪ Act2 , →, I1 × I2 , AP1 ∪ AP2 , L)where the transition relation → is defined by the following rules:α→1 s1s1 −−αs1 , s2 −−→ s1 , s2 andαs2 −−→2 s2αs1 , s2 −−→ s1 , s2 and the labeling function is defined by L(s1 , s2 ) = L(s1 ) ∪ L(s2 ).Parallelism and Communication39Example 2.19.Consider the two independent traffic lights described in Example 2.17 (page 36).