5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 19
Текст из файла (страница 19)
The intuitivemeaning of the above statement is that the process has to wait until the buffer for c isnonempty. If so, then it first performs the action c?x and then executes stmt. The useof communication actions in the guards leads to a more general class of program graphswith guards consisting of Boolean conditions on the variables or communication actions.For the case of an asynchronous channel the rules in Figure 2.20 on page 61 then have tobe extended by:c?x:α→ i ∧ len(ξ(c)) = k > 0 ∧ ξ(c) = v1 v2 . . . vki τ. . . , i , .
. . , η, ξ −→. . . , i , . . . , η , ξ 74Modelling Concurrent Systemswhere η = Effect(α, η[x := v1 ]) and ξ[c := v2 . . . vk ], andc!v:α→ i ∧ len(ξ(c)) = k < cap(c) ∧ ξ(c) = v1 . . . vki τ. . . , i , . . . , η, ξ −→. . . , i , . . . , η , ξ where η = Effect(α, η) and ξ[c := v1 . . . vk v].Another convenient concept is the special guard else which specifies configurations whereno other guarded command can be taken. The intuitive semantics of:if:: g1⇒ stmt1...⇒ stmtn:: gn:: else ⇒ stmtfiis that the else option is enabled if none of the guards g1 , . . . gn evaluates to true.
Inthis case, the execution evolves to a state in which the statement stmt is to be executed.Here, the gi ’s can be Boolean expressions on the variables or communication guards. Forexample,if :: d?x ⇒ stmt :: else ⇒ x := x + 1 fiincreases x unless a message is obtained from channel d. The else option used in loopsleads to nonterminating behaviors.Remark 2.41.Atomic RegionsThe axiom for atomic regions yields that if s = 1 . . .
, n , η, ξ is a state in the transitionsystem for the channel system associated with P = [P1 | . . . |Pn ] and i = atomic{x1 :=expr1 ; . . . ; xm := exprm }; . . . then in state s the ith process can perform the sequence ofassignments x1 := expr1 ; . . . ; xm := exprm in a single transition. With this semantics weabstract from the intermediate states that are passed when having performed the first iassignments (1 i < m) and avoid that other processes can interleave their activities withthese assignments.This concept can be generalized for atomic regions atomic{stmt} where the body stmt isan arbitrary statement.
The idea is that any terminating execution of stmt is collapsedinto a single transition, leading from a state with location stmt to a state with locationexit. For this more general approach, the semantic rule for atomic regions operates onexecution sequences in the transition system rather than just edges in the program graph.This is not problematic as one could provide the meaning of the statements on the levelof transition systems rather than program graph level. However, the semantics is lessParallelism and Communication75obvious for, e.g., infinite executions inside atomic regions, synchronous communicationactions inside atomic regions and blocking conditional commands inside atomic regions.One possibility is to insert transitions to a special deadlock state.
Another possibility is towork with a semantics that represents also the intermediate steps of an atomic region (butavoids interleaving) and to abort atomic regions as soon as a synchronous communicationis required or blocking configurations are reached.As we mentioned in the beginning of the section, Promela provides many more featuresthan nanoPromela, such as atomic regions with more complex statements than sequencesof assignments, arrays and other data types, and dynamic process creation. These conceptswill not be explained here and we refer to the literature on the model checker SPIN (see,e.g., [209]).2.2.6Synchronous ParallelismWhen representing asynchronous systems by transition systems, there are no assumptionsconcerning the relative velocities of the processors on which the components are executed.The residence time of the system in a state and the execution time of the actions arecompletely ignored.
For instance, in the example of the two independent traffic lights(see Example 2.17), no assumption has been made concerning the amount of time a lightshould stay red or green. The only assumption is that both time periods are finite. Theconcurrent execution of components is time-abstract.This is opposed to synchronous systems where components evolve in a lock step fashion.This is a typical computation mechanism in synchronous hardware circuits, for example,where the different components (like adders, inverters, and multiplexers) are connected toa central clock and all perform a (possibly idle) step on each clock pulse. As clock pulsesoccur periodically with a fixed delay, these pulses may be considered in a discrete manner,and transition systems can be adequately used to describe these synchronous systems.Synchronous composition of two transition systems is defined as follows.Definition 2.42.Synchronous ProductLet TSi = (Si , Act, →i , Ii , APi , Li ), i=1, 2, be transition systems with the same set ofactions Act.
Further, letAct × Act → Act, (α, β) → α ∗ β76Modelling Concurrent Systemsyr1xyORNOTr2TS1 :TS2 :0000111011TS1 ⊗ TS2 :000100101001110010111011Figure 2.23: Synchronous composition of two hardware circuits.be a mapping4 that assigns to each pair of actions α, β, the action name α ∗ β. Thesynchronous product TS1 ⊗ TS2 is given by:TS1 ⊗ TS2 = (S1 × S2 , Act, →, I1 × I2 , AP1 ∪ AP2 , L),where the transition relation is defined by the following ruleα→ 1 s1s1 −−∧βs2 −−→ 2 s2α∗βs1 , s2 −−−→ s1 , s2 and the labeling function is defined by: L(s1 , s2 ) = L1 (s1 ) ∪ L2 (s2 ).Action α∗β denotes the synchronous execution of actions α and β.
Note that compared tothe parallel operator where components perform actions in common synchronously, andother action autonomously (i.e., asynchronously), in TS1 ⊗ TS2 , both transition systemshave to perform all steps synchronously. There are no autonomous transitions of eitherTS1 or TS2 .4Operator ∗ is typically assumed to be commutative and associative.The State-Space Explosion ProblemExample 2.43.77Synchronous Product of Two CircuitsLet C1 be a circuit without input variables and with output variable y and register r.
Thecontrol functions for output and register transitions areλy = r1 , δr1 = ¬ r1 .Circuit C2 has input variable x , output variable y , and register variable r2 with thecontrol functionsλy = δr2 = x ∨ r2 .The transition system TSC1 ⊗ TSC2 is depicted in Figure 2.23 on page 76. Since actionnames are omitted for transition systems of circuits, action labels for TSC1 ⊗ TSC2 areirrelevant.
TSC1 ⊗ TSC2 is thus the transition system of the circuit with input variable x ,output variables y and y , and registers r1 and r2 , whose control functions are λy , λy , δr1 ,and δr2 .2.3The State-Space Explosion ProblemThe previous two sections have shown that various kinds of systems can be modeled usingtransition systems. This applies to program graphs representing data-dependent systems,and hardware circuits. Different communication mechanisms can be modeled in termsof appropriate operators on transition systems. This section considers the cardinality ofthe resulting transition systems, i.e., the number of states in these models.
Verificationtechniques are based on systematically analyzing these transition systems. The runtimesof such verification algorithms are mainly determined by the number of states of thetransition system to be analyzed. For many practical systems, the state space may beextremely large, and this is a major limitation for state-space search algorithms such asmodel checking.
Chapter 8, Section 6.7, and Chapter 7 introduce a number of techniquesto combat this problem.Program Graph Representation Transition systems generated by means of “unfolding” a program graph may be extremely large, and in some cases—e.g., if there areinfinitely many program locations or variables with infinite domains—even have infinitelymany states. Consider a program graph over the set of variables Var with x ∈ V ar.Recall that states of the unfolded transition system are of the form , η with location and variable evaluation η. In case all variables in Var have a finite domain, like bits,or bounded integers, and the number of locations is finite, the number of states in thetransition system is| dom(x) | .| Loc | ·x∈Var78Modelling Concurrent SystemsThe number of states thus grows exponentially in the number of variables in the programgraph: for N variables with a domain of k possible values, the number of states grows upto k N . This exponential growth is also known as the state-space explosion problem.It is important to realize that for even simple program graphs with just a small numberof variables, this bound may already be rather excessive.
For instance, a program graphwith ten locations, three Boolean variables and five bounded integers (with domain in{ 0, . . . , 9 }) has 10·23 ·105 = 8, 000, 000 states. If a single bit array of 50 bits is added tothis program graph, for example, this bound grows even to 800,000·250 ! This observationclearly shows why the verification of data-intensive systems (with many variables or complex domains) is extremely hard.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
