5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 20
Текст из файла (страница 20)
Even if there are only a few variables in a program, thestate space that must be analyzed may be very large.If dom(x) is infinite for some x ∈ Var, as for reals or integers, the underlying transitionsystem has infinitely many states as there are infinitely many values for x. Such program graphs usually yield undecidable verification problems.
This is not to say that theverification of all transition systems with an infinite state space is undecidable, however.It should be remarked that not only the state space of a transition system, but also thenumber of atomic propositions to represent program graphs (see Definition 2.15, page 34)may in principle be extremely large. Besides, any location, any condition on the variablesin the program graph is allowed as an atomic proposition. However, in practice, only asmall fragment of the possible atomic propositions is needed. An explicit representationof the labeling function is mostly not necessary, as the truth-values of the atomic formulaeare typically derived from the state information.
For these reasons, the number of atomicpropositions plays only a secondary role.For sequential hardware circuits (see page 26), states in the transition system are determined by the possible evaluations of the input variables and the registers. The size of thetransition system thus grows exponentially in the number of registers and input variables.For N input variables and K registers, the total state space consists of 2N +K states.Parallelism In all variants of parallel operators for transition systems and programgraphs, the state space of the complete system is built as the Cartesian product of thelocal state spaces Si of the components.
For example, for state space S of transitionsystemTS = TS1 ||| . . . ||| TSnwe have S = S1 × . . . × Sn where Si denotes the state space of transition system TSi .The state space of the parallel composition of a system with n states and a system withThe State-Space Explosion Problem79k states yields n·k states. The total state space S is thus|S1 | · .
. . · |Sn |.The number of states in S is growing (at most) exponentially in the number of components:the parallel composition of N components of size k each yields kN states. Even for smallparallel systems this may easily run out of control.Additionally, the variables (and their domains) represented in the transition system essentially influence the size of the state space. If one of the domains is infinite, then the statespace is infinitely large.
If the domains are finite, then the size of the state space growsexponentially in the number of variables (as we have seen before for program graphs).The “exponential blowup” in the number of parallel components and the number of variables explains the enormous size of the state space of practically relevant systems. Thisobservation is known under the heading state explosion and is another evidence for thefact that verification problems are particularly space-critical.Channel Systems For the size of transition systems of channel systems, similar observations can be made as for the representation of program graphs.
An important additionalcomponent for these systems is the size of the channels, i.e., their capacity. Clearly, ifone of these channels has an infinite capacity, this may yield infinitely many states inthe transition system. If all channels have finite capacity, however, the number of statesis bound in the following way. Let CS = [PG1 | . . . |PGn ] be a channel system overVar = Var1 ∪ . .
. ∪ Varn and channels Chan. The state space of CS is of cardinalityni=1| PGi | ·| dom(c) |cp(c) ,c∈Chanwhich can be rewritten as⎞⎛n⎝| Loci | ·| dom(x) |⎠ ·| dom(c) |cp(c) .i=1c∈Chanx∈VariFor L locations per component, K bit channels of capacity k each, and M variables x with| dom(x) | m totally, the total number of states in the transition system is Ln ·mM ·2K·k .This is typically enormous.Example 2.44.State-Space Size of the Alternating Bit ProtocolConsider a variant of the alternating bit protocol (see Example 2.32, page 57) where the80Modelling Concurrent Systemschannels c and d have a fixed capacity, 10 say.
Recall that along channel d, control bits aresent, and along channel c, data together with a control bit. Let us assume that data itemsare also simply bits. The timer has two locations, the sender eight, and the receiver six.As there are no further variables, we obtain that the total number of states is 2·8·6·410 ·210 ,which equals 3·235 . This is around 1011 states.2.4Summary• Transition systems are a fundamental model for modeling software and hardwaresystems.• An execution of a transition system is an alternating sequence of states and actionsthat starts in an initial state and that cannot be prolonged.• Interleaving amounts to represent the evolvement of “simultaneous” activities ofindependent concurrent processes by the nondeterministic choice between these activities.• In case of shared variable communication, parallel composition on the level of transition systems does not faithfully reflect the system’s behavior.
Instead, compositionon program graphs has to be considered.• Concurrent processes that communicate via handshaking on the set H of actionsexecute actions outside H autonomously whereas they execute actions in H synchronously.• In channel systems, concurrent processes communicate via FIFO-buffers (i.e., channels). Handshaking communication is obtained when channels have capacity 0.For channels with a positive capacity, communication takes place asynchronously—sending and receiving a message takes place at different moments.• The size of transition system representations grows exponentially in various components, such as the number of variables in a program graph or the number ofcomponents in a concurrent system.
This is known as the state-space explosionproblem.2.5Bibliographic NotesTransition systems. Keller was one of the first researchers that explicitly used transitionsystems [236] for the verification of concurrent programs. Transition systems are usedBibliographic Notes81as semantical models for a broad range of high-level formalisms for concurrent systems,such as process algebras [45, 57, 203, 298, 299], Petri nets [333], and statecharts [189].
Thesame is true for hardware synthesis and analysis, in which variants of finite-state automata(Mealy and Moore automata) play a central role; these variants can also be described bytransition systems [246]. Program graphs and their unfolding into transition systems havebeen used extensively by Manna and Pnueli in their monograph(s) on temporal logicverification [283].Synchronization paradigms. Shared variable “communication” dates back to the midsixties and is due to Dijkstra [126]. He also coined the term interleaving in 1971 [128].Handshaking communication has been the main interaction paradigm in process algebrassuch as ACP [45], CCS [298, 299], CSP [202, 203], and LOTOS [57]. For a detailedaccount of process algebra we refer to [46].
The principle of synchronized parallelism hasbeen advocated in Milner’s synchronous variant of CCS, SCCS [297], and is used by Arnoldto model the interaction between finite transition systems [19]. Synchronous parallelism isalso at the heart of Lustre [183], a declarative programming language for reactive systems,and is used in many other hardware-oriented languages.The interaction between concurrent processes by means of buffers (or channels) has firstbeen considered by Dijkstra [129].
This paradigm has been adopted by specification languages for communication protocols, such as SDL (Specification and Description Language [37]) which is standardized by the ITU. The idea of guarded command languagesgoes back to Dijkstra [130]. The combination of guarded command languages in combination with channel-based communication is also used in Promela [205], the input languageof the model checker SPIN [208].
The recent book by Holzmann [209] gives a detailedaccount of Promela and SPIN. Structured operational semantics has been introduced byPlotkin [334, 336] in 1981. Its origins are described in [335]. Atomic regions have been firstdiscussed by Lipton [276], Lamport [257] and Owicki [317]. Further details on semanticrules for specification languages for reactive systems can be found, e.g., in [15, 18].The examples.
Most examples that have been provided in this chapter are rather classical.The problem of mutual exclusion was first proposed in 1962 by Dekker together with analgorithm that guarantees two-process mutual exclusion. Dijkstra’s solution [126] was thefirst solution to mutual exclusion for an arbitrary number of processes. He also introducedthe concept of semaphores [127] and their use for solving the mutual exclusion problem.A simpler and more elegant solution has been proposed by Lamport in 1977 [256]. Thiswas followed up by Peterson’s mutual exclusion protocol [332] in 1981.
This algorithm isfamous by now due to its beauty and simplicity. For other mutual exclusion algorithms,see e.g. [283, 280]. The alternating bit protocol stems from 1969 and is one of the first flowcontrol protocols [34]. Holzmann gives a historical account of this and related protocolsin his first book [205].822.6Modelling Concurrent SystemsExercisesExercise 2.1. Consider the following two sequential hardware circuits:x1ORy1x2ANDy2NOTANDORr1r2Questions:(a) Give the transition systems of both hardware circuits.(b) Determine the reachable part of the transition system of the synchronous product of thesetransition systems. Assume that the initial values of the registers are r1 =0 and r2 =1.Exercise 2.2. We are given three (primitive) processes P1 , P2 , and P3 with shared integervariable x.
The program of process Pi is as follows:Algorithm 1 Process Pifor ki = 1, . . . , 10 doLOAD(x);INC(x);STORE(x);odThat is, Pi executes ten times the assignment x := x+1. The assignment x := x+1 is realizedusing the three actions LOAD(x), INC(x) and STORE(x). Consider now the parallel program:Algorithm 2 Parallel program Px := 0;P1 || P2 || P3Question: Does P have an execution that halts with the terminal value x = 2?Exercise 2.3. Consider the following street junction with the specification of a traffic light asoutlined on the right.Exercises83A1Ai :redA2yellowA2red/yellowgreenA1A3(a) Choose appropriate actions and label the transitions of the traffic light transition systemaccordingly.(b) Give the transition system representation of a (reasonable) controller C that switches thegreen signal lamps in the following order: A1 , A2 , A3 , A1 , A2 , A3 , .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
