9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Compositional and symbolic model-checking of real-time systems

Basic Research in Computer Science

BRICS

BRICS RS-96-59 Larsen et al.: Compositional and Symbolic Model-Checking of Real-Time Systems

Compositional and Symbolic Model-Checking of Real-Time Systems

Kim G. Larsen Paul Pettersson Wang Yi

BRICS Report Series ISSN 0909-0878

RS-96-59 December 1996

Copyright c 1996, BRICS, Department of Computer Science University of Aarhus. All rights reserved. Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting: BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk BRICS publications are in general accessible through World Wide Web and anonymous FTP: http://www.brics.dk/ ftp://ftp.brics.dk/ This document in subdirectory RS/96/59/

Compositional and Symbolic Model-Checking of Real-Time Systems?

Kim G. Larsen? Paul Pettersson? Uppsala University

Abstract

E?cient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill. However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clockvariables. In this paper we attack these explosion problems by developing and combining compositional and symbolic model-checking techniques. The presented techniques provide the foundation for a new automatic veri?cation tool Uppaal. Experimental results indicate that Uppaal performs time- and space-wise favorably compared with other real-time veri?cation tools.

Wang Yi?

1

Introduction

Within the last decade model-checking has turned out to be a useful technique for verifying temporal properties of ?nite-state systems. E?cient model-checking algorithms for ?nite-state systems have been obtained with respect to a number of logics. However, the major problem in applying model-checking even to moderatesize systems is the potential combinatorial explosion of the state space arising from parallel composition. In order to avoid this problem, algorithms have been sought that avoid exhaustive state space exploration, either by symbolic representation of the states space using Binary Decision Diagrams [1], by application of

? The work has been supported by the European Communities under CONCUR2, BRA 7166, NUTEK (Swedish Board for Technical Development) and TFR (the Swedish Technical Research Council). ? On leave from BRICS and the Department of Mathematics and Computer Science, Aalborg University, Fredrik Bajers Vej 7–E, DK–9220 Aalborg, Denmark. E-mail: kgl@iesd.auc.dk. ? Department of Computer Systems, Box 325, Uppsala University, S751 05, Uppsala, Sweden. E-mail: {paupet,yi}@docs.uu.se.

partial order methods [2, 3] which suppresses unnecessary interleavings of transitions, or by application of abstractions and symmetries [4, 5, 6]. In the last few years, model-checking has been extended to real-time systems, with time considered to be a dense linear order. A timed extension of ?nite automata through addition of a ?nite set of realvalued clock-variables has been put forward [7] (so called timed automata), and the corresponding modelchecking problem has been proven decidable for a number of timed logics including timed extensions of CTL (TCTL) [8] and timed ?-calculus (T? ) [9]. A state of a timed automaton is of the form (l, u), where l is a control-node and u is a clock-assignment holding the current values of the clock-variables. The crucial observation made by Alur, Courcoubetis and Dill and the foundation for decidability of model-checking is that the (in?nite) set of clock-assignments may e?ectively be partitioned into ?nitely many regions in such a way that clock-assignments within the same region induce states satisfying the same logical properties. Model-checking of real-time systems based on the region technique su?ers two potential types of explosion arising from parallel composition: Explosion in the region space, and Explosion in the space of control-nodes. We attack these problems by development and combination of two new veri?cation techniques: 1. A symbolic technique reducing the veri?cation problem to that of solving simple constraint systems (on clock-variables), and 2. A compositional quotient construction, which allows components of a real-time system to be gradually moved from the system description into the speci?cation. The intermediate speci?cations are kept small using minimization heuristics. The property-independent nature of regions leads to an extremely ?ne (and large) partitioning of the set of clock-assignments. Our symbolic technique allows the partitioning to take account of the particular property

to be veri?ed and will thus in practice be considerably coarser (and smaller). For the explosion on control-nodes, recent work by Andersen [10] on (untimed) ?nite-state systems gives experimental evidence that the quotient technique improves results obtained using Binary Decision Diagrams [1]. Our aim in this paper is to make this new successful compositional model-checking technique applicable to real-time systems. For example, consider the following typical model-checking problem A1 | . . . | An |= ? where the Ai ’s are timed automata. We want to verify that the parallel composition of these satis?es the formula ? without having to construct the complete control-node space of (A1 | . . . | An ). We will avoid this complete construction by removing the components Ai one by one while simultaneously transforming the formula accordingly. Thus, when removing the component An we will transform the formula ? into the quotient formula ? / An such that A1 | . . . | An?1 |= ? / An (1) Now clearly, if the quotient is not much larger than the original formula we have succeeded in simplifying the problem. Repeated application of quotienting yields A1 | . . . | An |= ? i? 1 |= ? / An /An?1 / . . . / A1 (2) where 1 is the unit with respect to parallel composition. However, these ideas alone are clearly not enough as the explosion may now occur in the size of the ?nal formula instead. The crucial and experimentally “veri?ed” observation by Andersen was that each quotienting should be followed by a minimization of the formula based on a small collection of e?ciently implementable strategies. In our setting, Andersen’s collection is extended to include strategies for propagating and simplifying timing constraints. Our new symbolic and compositional veri?cation technique is developed for a real-time logic designed speci?cally for expressing safety and bounded liveness properties. Comparatively less expressive than TCTL and T? , the logic is still su?ciently expressive for practical purposes, and the logic allows a number of operators of other logics to be derived. Most importantly, the somewhat restrictive expressive power of our logic allows for e?cient model-checking as demonstrated by our experimental results, which includes a comparison with other existing automatic veri?cation tools for realtime systems (HyTech, Kronos and Epsilon). 2 A1 | . . . | An |= ? i?

For the logics TCTL and T? , [9] o?ers a symbolic veri?cation technique. However, due to the high expressive power of these logics the partitioning employed in [9] is signi?cantly ?ner (and larger) and implementation-wise more complicated than the symbolic technique we present in this paper. Our symbolic method is based on the constraint solving technique presented in [11], where the technique was developed for simple reachability problems. An initial e?ort in applying the compositional quotienting technique to real-time systems has been given in [12]. This work also contains experimental evidence of the potential bene?ts of the quotient technique in a real-time setting. However, being based directly on the (very ?ne) notion of regions, [12] su?ers from a potential explosion in the region-space. The outline of this paper is as follows: In the next section we give a short presentation of the notions of timed automata and networks; in section 3, the safety logic is presented and its expressive power is illustrated. Section 4 describes the symbolic veri?cation technique based on constraint solving and section 5 describes the compositional quotienting technique. Both techniques are illustrated by an example. In section 6, we report on our experimental results, which indicate that Uppaal performs time- and space-wise favorably compared with other real-time veri?cation tools.

2

Real-Time Systems

We shall use timed transition systems as a basic semantic model for real-time systems. The type of systems we are studying will be a particular class of timed transition systems that are syntactically described by networks of timed automata [11, 12].

2.1

Timed Transition Systems

A timed transition system is a labelled transition system with two types of labels: atomic actions and delay actions (i.e. positive reals), representing discrete and continuous changes of real-time systems. Let Act be a ?nite set of actions ranged over by a, b etc, and P be a set of atomic propositions ranged over by p, q etc. We use R to stand for the set of nonnegative real numbers, ? for the set of delay actions { (d) | d ∈ R}, and L for the union Act ∪ ?. De?nition 1 A timed transition system over Act and P is a tuple S = S, s0 , ?→, V , where S is a set of states, s0 is the initial state, ?→? S × L × S is a

transition relation, and V : S → 2P is a proposition assignment function. 2 Note that the above de?nition is standard for labelled transition systems except that we introduced a proposition assignment function V , which for each state s ∈ S assigns a set of atomic propositions V (s) that hold in s. In order to study compositionality problems we introduce a parallel composition between timed transition systems. Following [13] we suggest a composition parameterized with a synchronization function generalizing a large range of existing notions of parallel compositions. A synchronization function f is a partial function (Act ∪ {0}) × (Act ∪ {0}) → Act, where 0 denotes a distinguished no-action symbol1 . Now, let Si = Si , si,0 , ?→i , Vi , i = 1, 2, be two timed transition systems and let f be a synchronization function. Then the parallel composition S1 |f S2 is the timed transition system S, s0 , ?→, V , where s1 |f s2 ∈ S whenever s1 ∈ S1 and s2 ∈ S2 , s0 = s1,0 |f s2,0 , ?→ is inductively de?ned as follows: ? s1 |f s2 ?→ s1 |f s2 if s1 ?→1 s1 , s2 ?→2 s2 and f (a, b) = c ? s1 |f s2 ?→ s1 |f s2 if s1 ?→1 s1 and s2 ?→2 s2 and ?nally, the proposition assignment function V is de?ned by V (s1 |f s2 ) = V1 (s1 ) ∪ V2 (s2 ). Note also that the set of states and the transition relation of a timed transition system may be in?nite. We shall use networks of timed automata as a ?nite syntactical representation to describe timed transition systems.

(d) (d) (d) c a b

to stand for the set of formulas ranged over by g , generated by the following syntax: g ::= c | g ∧ g , where c is an atomic constraint of the form: x ? n or x ? y ? n for x, y ∈ C , ?∈ {≤, ≥, =, <, >} and n being a natural number. We shall call B (C ) clock constraints or clock constraint systems over C . 2 We shall use tt to stand for a constraint like x ≥ 0 which is always true, and ff for a constraint x < 0 which is always false as clocks can only have non-negative values. De?nition 3 A timed automaton A over actions Act, atomic propositions P and clocks C is a tuple N, l0 , E, I, V . N is a ?nite set of nodes (controlnodes), l0 is the initial node, and E ? N × B (C ) × Act × 2C × N corresponds to the set of edges. In the g,a,r case, l, g, a, r, l ∈ E we shall write, l ?→ l which represents an edge from the node l to the node l with clock constraint g (also called the enabling condition of the edge), action a to be performed and the set of clocks r to be reset. I : N → B (C ) is a function which for each node assigns a clock constraint (also called the invariant condition of the node), and ?nally, V : N → 2P is a proposition assignment function which for each node gives a set of atomic propositions true in the node. 2 Note that for each node l, there is an invariant condition I (l) which is a clock constraint. Intuitively, this constraint must be satis?ed by the system clocks whenever the system is operating in that particular controlnode. Informally, the system starts at node l0 with all its clocks initialized to 0. The values of the clocks increase synchronously with time at node l as long as they satisfy the invariant condition I (l). At any time, the aug,a,r tomaton can change node by following an edge l ?→ l provided the current values of the clocks satisfy the enabling condition g . With this transition the clocks in r get reset to 0. Example 1 Consider the automata Am , Bn and Cm,n in Figure 1 where m, n, m , n are natural numbers. We use m, n, m , n as parameters. The automaton Cm,n has four nodes, l0 , l1 , l2 and l3 , two clocks x and y , and three edges. The edge between l1 and l2 has b as action, {x, y } as reset set and the enabling condition for the edge is x ≥ m. The invariant conditions for nodes l1 and l2 are x ≤ m and y ≤ n respectively. 2 Now we introduce the notion of a clock assignment. Formally, a clock assignment u for C is a function from C to R. We denote by RC the set of clock assignments for C . For u ∈ RC , x ∈ C and d ∈ R, u + d denotes 3

2.2

Networks of Timed Automata

A timed automaton [7] is a standard ?nite-state automaton extended with a ?nite collection of real-valued clocks2 . Conceptually, the clocks may be considered as the system clocks of a concurrent system. They are assumed to proceed at the same rate and measure the amount of time that has been elapsed since they were reset. The clocks values may be tested (compared with natural numbers) and reset (assigned to 0). De?nition 2 (Clock Constraints) Let C be a set of real-valued clocks ranged over by x, y etc. We use B (C )

1 We

extend the transition relation of a timed transition sys0

tem such that s ?→ s i? s = s . 2 Timed transition systems may alternatively be described using timed process calculi.

Am :

h0 :

t t

Bn :

k0 :

t t

Cm,n :

l0 :

t t

tt a {x}

x ≤ m

Note that we need to assume that m ≤ e ≤ m and n ≤ f ≤ n because of the invariant conditions on l1 and l2 . 2 Parallel composition may now be extended to timed automata in the obvious way: for two timed automata A and B and a synchronization function f , the parallel composition A |f B denotes the timed transition system SA |f SB . Note that the timed transition system SA |f SB can also be represented ?nitely as a timed automaton. In fact, one may e?ectively construct the product automaton A ?f B such that its timed transition system SA?f B is bisimilar to SA |f SB . The nodes of A ?f B is simply the product of A’s and B ’s nodes, the invariant conditions on the nodes of A ?f B are the conjunctions of the conditions on respective A’s and B ’s nodes, the set of clocks is the (disjoint) union of A’s and B ’s clocks, and the edges are based on synchronizable A and B edges with enabling conditions conjuncted and reset-sets unioned. Example 3 Let f be the synchronization function de?ned by f (a, 0) = a, f (b, b) = b and f (0, c) = c. Then the automaton Cm,n in Figure 1 is isomorphic to the part of Am ?f Bn which is reachable from (h0 , k0 ). 2

tt a {x}

x ≤ m

tt b {y }

y ≤ n

l1 :

h1 :

k1 :

b

x≥m {x, y }

b

x≥m {x}

c

y≥n {y }

y ≤ n

l2 :

h2 :

t t

k2 :

t t

c

y≥n {y }

l3 :

t t

Figure 1: Three timed automata the time assignment which maps each clock x in C to the value u(x) + d. For C ? C , [C → 0]u denotes the assignment for C which maps each clock in C to the value 0 and agrees with u over C \C . Whenever u ∈ RC , v ∈ RK and C and K are disjoint, we use uv to denote the clock assignment over C ∪ K such that (uv )(x) = u(x) if x ∈ C and (uv )(x) = v (x) if x ∈ K . Given a clock constraint g ∈ B (C ) and a clock assignment u ∈ RC , g (u) is a boolean value describing whether g is satis?ed by u or not. When g (u) is true, we shall say that u is a solution of g . A state of an automaton A is a pair (l, u) where l is a node of A and u a clock assignment for C . The initial state of A is (l0 , u0 ) where u0 is the initial clock assignment mapping all clocks in C to 0. The semantic of A is given by the timed transition system SA = S, σ0 , ?→, V , where S is the set of states of A, σ0 is the initial state (l0 , u0 ), ?→ is the transition relation de?ned as follows: ? (l, u)?→(l , u ) if there exist r, g such that l ?→ l , g (u) and u = [r → 0]u ? (l, u)?→(l , u ) if (l = l ), u = u + d and I (u ) and V is extended to S simply by V (l, u) = V (l). Example 2 Reconsider the automaton Cm,n of Figure 1. Assume that d ≥ 0, m ≤ e ≤ m and n ≤ f ≤ n . We have the following typical transition sequence:

(l0 , (0, 0)) ?→ (l0 , (d, d)) ?→ (l1 , (0, d)) ?→ (l1 , (e, d + e)) ?→ (l2 , (0, 0)) ?→ (l2 , (f, f )) ?→ (l3 , (f, 0))

b (f ) c (d) a (e)

3

A Logic for Safety and Bounded Liveness Properties

It has been pointed out [14, 11], that the practical goal of veri?cation of real-time systems, is to verify simple safety properties such as deadlock-freeness and mutual exlusion. Our previous work [11] shows that such properties can be veri?ed on-the-?y by simple reachability analysis which avoids construction of the whole reachable state-space of systems.

3.1

Syntax and Semantics

a

g,a,r

(d)

We shall present a timed modal logic to specify safety properties. In fact, the logic can also be used to specify bounded liveness properties such as “whenever p becomes true, q will be true within a given time bound”. The logic may be seen as a fragment of the timed ?calculus presented in [9], and also studied in [15]. De?nition 4 Let K be a ?nite set of clocks. We shall call K formula clocks. Let Id be a set of identi?ers. The set Ls of formulas over K , Id, Act, and P is generated by the abstract syntax with ? and ψ ranging over Ls : ? ::= cp | cp ∨ ? | ? ∧ ψ | ? ?? | [a] ? | z in ? | Z

4

where cp may be an atomic clock constraint c in the form of x ? n or x ? y ? n for x, y ∈ K and natural number n, or an atomic proposition p ∈ P , a ∈ Act (an action), z ∈ K and Z ∈ Id (an identi?er). 2 As before, we shall use tt to stand for a formula like x ≥ 0 which is always true, and ff for a formula x < 0 which is always false for a formula clock x ∈ K . Note that the logic is essentially the fragment of the timed modal logic presented in [15] by eliminating existential quanti?cation over delay transitions, general disjunction over formulas, and existential quanti?cation over a-transitions. We do allow a simple form of disjunction, in that a clock constraint or an atomic proposition may be disjuncted with an arbitrary formula. We disallow general disjunction in the logic to achieve e?cient compositional and symbolic model-checking algorithms. However, the logic is expressive enough to specify safety and bounded liveness properties. We shall see, that the simple form of disjunction allows us to specify bounded liveness properties such as “p will be true within n”. The meaning of the identi?ers is speci?ed by a declaration D assigning a formula of Ls to each identi?er. def When D is understood we write Z = ? for D(Z ) = ?. Given a timed transition system S = S, s0 , ?→, V described by a network of timed automata, we interpret the Ls formulas over an extended state s, u where s ∈ S is a state of S , and u is a clock assignment for K . A formula of the form: x ? m and x ? y ? n is satis?ed by an extended state s, u if the values of x, y in u satisfy the required relationship. Informally, an extended state s, u satis?es ? ? means that all future states reachable from s, u by delays will satisfy property ?; ? ? denotes universal quanti?cation over delay transitions. Similarly, a state s, u satis?es [a]? means that all intermediate states reachable from s, u by an a-transition (performed by s will satisfy property ?; [a] denotes universal quanti?cation over a-transitions. The formula (x in ?) initializes the formula clock x to 0; i.e. an extended state satis?es the formula in case the modi?ed state with x being reset to 0 satis?es ?. Finally, an extended state satis?es an identi?er Z if it satis?es the corresponding declaration (or de?nition) D(Z ). Let D be a declaration. Formally, the satisfaction relation |=D between extended states and formulas is de?ned as the largest relation satisfying the implications of Table 1. Any relation satisfying the implications in Table 1 is called a satis?ability relation. It follows from standard ?xpoint theory [16] that |=D is the union of all satis?ability relations. For simplicity, we shall omit the index D and write |= instead of |=D whenever it is understood from the context. 5

s, u |= c s, u |= p s, u |= cp ∨ ? s, u |= ? ∧ ψ

? c(u) ? p ∈ V (s) ? s, u |= cp or s, u |= ? ? s, u |= ? and s, u |= ψ

(d)

s, u |= ? ?? ? ?d, s : s ?→ s ? s , u + d |= ? a s, u |= [a] ? ? ?s : s ?→ s ? s , u |= ? s, u |= x in ? ? s, v |= ? where v = [{x} → 0]v s, u |= Z ? s, u |= D(Z ) Table 1: De?nition of satis?ability. We say that S satis?es a formula ? and write S |= ? when s0 , v0 |= ? where s0 is the initial state of S and v0 is the assignment with v0 (x) = 0 for all x. Similarly, we say that a timed automaton A satis?es ? in case SA |= ?. We write A |= ? in this case. Example 4 Consider the following declaration F of the identi?ers Xi and Zi where i is a natural number. ? ? def ? ? Xi = [a] z in Zi ? ? ? ? def F= Zi = at(l3 ) ∨ ? ? ? ? ? z < i ∧ [a]Zi ∧ [b]Zi ∧ [c]Zi ∧ ? ?Zi ? Assume that at(l3 ) is an atomic proposition meaning that the system is operating in control-node l3 . Then, Xi expresses the property that after an a-transition, the system must reach node l3 within i time units. Now, reconsider the automata Am , Bn and Cm,n of Figure 1. It may be argued that Cm,n |= Xm +n and (consequently), that Am |f Bn |= Xm +n . 2

3.2

Derived Operators

The property Zi described in Example 3 is an attempt to specify bounded liveness properties: namely that a certain proposition must be satis?ed within a given time bound. We shall use the more informative notation at(l3 ) BEFORE i to denote Zi . In the following, we shall present several such intuitive operators that are de?nable in our logic. For simplicity, we shall assume that the set of actions Act is a ?nite set {a1 ...am }, and use [Act]? to denote the formula [a1 ]? ∧ ... ∧ [am ]?. Now, let ? be a general formula, cp be an atomic clock constraint or an atomic proposition and n be a natural number. A collection of derived operators are given in Table 2.

INV(?) ? UNTIL cp

≡ X where X = ? ∧ ? ?X ∧ [Act]X ≡ X where X = cp ∨ ? ∧ ? ?X ∧ [Act]X

def

def

? UNTIL<n cp ≡ z in (? ∧ z < n) UNTIL cp cp BEFORE n ≡ tt UNTIL<n cp Table 2: Derived Operators The intuitive meanings of these operators are as follows: INV(?) is satis?ed by a timed automaton means that the automaton must enjoy the property ? now, and for all future time points, the reachable states should satisfy INV(?) (i.e. X ), and after any action transition, the reachable states should again satisfy INV(?) (i.e. X ): namely that ? is an invariant property of the automaton. ? UNTIL cp is satis?ed by a timed automaton means that the automaton enjoys the property cp now, or otherwise all reachable states by action transitions and delay transitions should satisfy ?. This simply means that ? must hold at least before cp becomes true. The bounded version of the UNTIL construct ? UNTIL<n cp is similar to ? UNTIL cp except that cp must be true within n time units. A simpler version of this operator is cp BEFORE n meaning that property cp must be true within n time units. Alternatively, ? UNTIL<n cp can be de?ned as z in X def where X = cp ∨ ? ∧ (x < n) ∧ ? ?X ∧ [Act]X .

Recall that a semantical state of a network of timed automata is a pair (l, u) where l is a control-node and u ∈ RC is a clock assignment. The model-checking problem is in general to check whether an extended state in the form (l, u), v satis?es a given formula ?, that is, (l, u), v |= ? Note that u is a clock assignment for the automata clocks and v is a clock assignment for the formula clocks. Now, the problem is that we have too many (in fact, in?nitely many) such assignments to check in order to conclude (l, u), v |= ?. In this section, we shall use clock constraints B (C ∪ K ) for automata clocks C and formula clocks K , as de?ned in section 2 to symbolically represent clock assignments. We shall use D to range over B (C ∪ K ). Instead of checking (l, u), v |= ? for each u and v , we develop an algorithm to simultaneously check [l, D] |= ? which means that for each u and v such that uv is a solution to the constraint system D, we have (l, u), v |= ?. Thus the space RC ∪K is partitioned in terms of clock constraints. As for a given network and a given formula, we have only ?nite many such constraints to check, the problem becomes decidable, and in fact as the partitioning takes account of the particular property, the number of partitions is in practice considerably smaller compared with the region-technique.

4

Symbolic Model-Checking

We have presented a model to describe real-time systems, i.e. networks of timed automata, and a logic to specify properties of such systems. The next question is how to check whether a given formula in the logic is satis?ed by a given network of automata. This is the so-called model-checking problem. As the systems we are studying are in general in?nite-state due to the real-valued clocks, we need e?cient methods to represent the state-space symbolically. The region-graph technique by Alur, Courcoubetis and Dill allows the state space of a real time system to be partitioned into ?nitely many regions in such a way that states within the same region satisfy the same properties. It follows that model-checking is decidable as the region partitioning enables standard ?nite-state algorithmic modelchecking techniques to be applied. However, as the notion of region is property-independent and the number of such regions depends on the constants used in the clock constraints of an automaton, this leads to an extremely ?ne (and large) partitioning. 6

4.1

Operations on Clock Constraints

To develop the model-checking algorithm, we need a few operations to manipulate clock constraints. Given a clock constraint D, we shall call the set of clock assignments satisfying D, the solution set of D. De?nition 5 Let A and A be the solution sets of clock constraints D, D ∈ B (C ∪ K ). We de?ne A↑ A↓ {x}A A∧A = = = = {w + d | w ∈ A and d ∈ R} {w |?d ∈ R : w + d ∈ A} {[{x} → 0]w | w ∈ A} {w | w ∈ A and w ∈ A }

2

First, note that A ∧ A is simply the intersection of the two sets. Consider the set A for the case of two clocks, shown in (a) of Figure 2. The three operations A↑ , A↓ and {x}A are illustrated in (b), (c) and (d) respectively of Figure 2. Intuitively, A↓ is the largest

set of time assignments that will eventually reach A after some delay; whereas A↑ is the dual of A↓ : namely that it is the largest set of time assignments that can be reached by some delay from A. Finally, {y }A is the projection of A down to the x-axis. We extend the projection operator to sets of clocks. Let r = {x1 ...xn } be a set of clocks. We de?ne r(A) recursively by {}(A) = A and {x1 ...xn }(A) = {x1 }({x2 ...xn }A). The following Proposition establishes that the class of clock constraints B (C ∪ K ) is closed under the four operations de?ned above. Proposition 1 Let D, D ∈ B (C ∪ K ) with solution sets A and A , and x ∈ C ∪ K . Then there exist D1 , D2 , D3 , D4 ∈ B (C ∪ K ) with solution sets A↑ , A↓ , {x}A and A ∧ A respectively. 2 In fact, the resulted constraints Di ’s can be e?ectively constructed from D and D , as shown in section 4.3. In order to save notation, from now on, we shall simply use D↑ , D↓ , {x}D and D ∧ D to denote the clock constraints which are guaranteed to exist due to the above proposition. We will also need a few predicates over clock constraints for the model-checking procedure. We write D ? D to mean that the solution set of D is included in the solution set of D and D = ? to mean that the solution set of D is empty.

D=? [l, D] [l, D] [l, D] [l, D] [l, D] [l, D] [l, D] [l, D] [l, D]

c p c∨? p∨? ?1 ∧ ?2 [a] ? ? ?? x in ? Z

? ? ? ? ? ? ?

[l, D] ? D?c p ∈ V (s) [l, D ∧ ?c] ? [l, D] p or [l, D] ? [l, D] ?1 and [l, D] ?2 [l , r(D ∧ g )] ? whenever g,a,r l ?→ l ? [l, D] ? and [l, (D ∧ I (l))↑ ∧ I (l)] ? ? [l, {x}D] ? ? [l, D] D(Z )

Table 3: De?nition of symbolic satis?ability. Theorem 2 Let A be a timed automaton over clock set C and ? a formula over K . Then the following holds: A |= ? if and only if [l0 , D0 ] ?

where l0 is the initial node of A and D0 is the linear constraint system {x = 0 | x ∈ C ∪ K }. Proof: It is proved by co-induction (on ) that [l, D] ? holds precisely when (l, u), v |= ? for all uv in D.

4.2

Model-Checking by Constraint Solving

2

Given a network of timed automaton A over clocks C , we shall interprete formulas over clocks K with respect to symbolic states of the form [l, D] where l is a control-node of A and D is a clock constraint of B (C ∪ K ). Let D be a declaration. The symbolic satisfaction relation D between symbolic states and formulas is de?ned as the largest relation satisfying the implications in Table 3. We call a relation satisfying the implications in Table 3 a symbolic satis?ability relation. Again, it follows from standard ?xpoint theory [16] that D is the union of all symbolic satis?ability relations. For simplicity, we shall omit the index D and write instead of D whenever it is understood from the context. The following Theorem shows that the symbolic interpretation of Ls in Table 3 expresses the su?cient and necessary conditions for a timed automata to satisfy a formula ?3 .

3 Note that Theorem cannot be extended to a logic with general disjunction (or existential quanti?cations): the obvious requirement that [l, D] |= ?1 ∨ ?2 should imply either [l, D] |= ?1 or [l, D] |= ?2 will fail to satisfy the Theorem.

Given a symbolic satisfaction problem [l, D] ? we may determine its validity by using the implications of Table 3 as rewrite rules. Due to the maximal ?xed point property of , rewriting may be terminated successfully in case cycles are encountered. As the rewrite graph of any given problem [l, D] ? can be shown to be ?nite this yields a decision procedure for model checking. The operations and predicates on clock constraint systems discussed in Section 4.1 can be e?ciently implemented by representing constraint systems as weighted directed graphs. The basic idea is to use a shortest-path algorithm to close a constraint system under entailment so that operations and predicates can be easily computed [17].

5

Compositional Model-Checking

The symbolic model-checking presented in the previous section provides an e?cient way to deal with the potential explosion caused by the addition of clocks. However, a potential explosion in the node-space due to parallel composition still remains. In this section we attack this problem by development of a quotient 7

y

y

y A↑

y

A A↓

(a)

A {y }A

(b)

x

x

(c)

x

(d)

x

Figure 2: Operations on Solution Sets construction, which allows components to be gradually moved from the parallel system into the speci?cation, thus avoiding explicit construction of the global node space. The intermediate speci?cations are kept small using minimization heuristics. Recent experimental work by Andersen [10] demonstrates that for (untimed) ?nite-state systems the quotient technique improves results obtained using Binary Decision Diagrams. Also, an initial experimental investigation of the quotient technique to real-time systems in [12] has indicated that these promising results will carry over to the setting of real-time systems. In this section we shall provide a new (and compared with [12] simple) quotient construction and show how to integrate it with the symbolic technique of the previous section.

c l

f

= c = tt p

f

p l

f

; p ∈ V (l) ; p ∈ V (l) l) ∧ (?2

f

(?1 ∧ ?2 ) l

f

= (?1

l)

(? ??) l

f

= ? ? I (l) ? (? l)

f

(x in ?) l

f

= x in (? l)

f

(c ∨ ?) l

f

= (c l) ∨ (? l)

f f

(p ∨ ?) l

f

= (p l) ∨ (? l)

f f

([a]?) l

f

=

l? → l ∧ f (b,c)=a

g,c,r

g ? [b](r in ? l )

f

5.1

Quotient Construction

X

f

l

= Xl where Xl = D (X ) l

f

def

Given a formula ?, and two timed automata A and B we aim at constructing a formula (called the quotient) ? B such that

f

Table 4: De?nition of Quotient ? l

f

A |f B |= ? if and only if A |= ? B

f

(3)

The bi-implication indicates that we are moving parts of the parallel system into the formula. Clearly, if the quotient is not much larger than the original formula, we have simpli?ed the task of model-checking, as the (symbolic) semantics of A is signi?cantly smaller than that of A |f B . More precisely, whenever ? is a formula over K , B is a timed automaton over C and l is a node of B , we de?ne the quotient formula ? l over C ∪ K

f

in Table 4 on the structure of ?45 .

4 For g = c ∧ . . . c a clock constraint we write g ? ? as n 1 an abbreviation for the formula ?c1 ∨ . . . ∨ ?cn ∨ ?. This is an Ls -formula as atomic constraint are closed under negation. 5 In the rule for [a]?, we assume that all nodes l of a timed tt,0,? automaton are extended with a 0-edge l ?→ l.

The quotient ? l expresses the su?cient and necf essary requirement to a timed automaton A in order that the parallel composition A |f B with B at node l satis?es ?. In most cases quotienting simply distributes with respect to the formula construction. The quotient construction for ? ?? re?ects that A |f B can only delay provided I (l) is satis?ed. The quotient construction for [a]? must quantify over all actions of A which can possibly lead to an a-transition of A |f B : according to the semantics of parallel composition, b is such an action provided B (at node l) can perform a synchronizable g,c,r action c (according to some edge l ?→ l ) such that f (b, c) = a. The guard as well as the reset set of the g,c,r involved A-edge l ?→ l is re?ected in the quotient formula. Note that the quotient construction for identi?ers 8

introduces new identi?ers of the form Xl . These new def identi?ers and their de?nitions (Xl = D(X ) l) are f collected in the (quotient) declaration D B . For l0 the initial node of a timed automaton B , the quotient ? l0 expresses the su?cient and necessary f requirement to a timed automaton A in order that the parallel composition A |f B satis?es ?. This is stated in the following Theorem 3: Theorem 3 Let A and B be two timed automata and let l0 be the initial node of B . Then A |f B |=D ? if and only if A |=D B ? l0

f

??? D?c D ? ([a]?) D ? (?1 ∧ ?2 ) D ? (x in ?) D ? (p ∨ ?) D ? (c ∨ ?) D ? (? ??) D?X

≡ ≡ ≡ ≡ ≡ ≡ ≡ ≡ ≡

tt tt ; if D ? c [a](D ? ?) (D ? ?1 ) ∧ (D ? ?2 ) x in ({x}D ? ?) p ∨ (D ? ?) (D ∧ ?c) ? ? ? ?(D↑ ? ?) ; if D↓ ? D D ? D(X )

Table 5: Constraint Propagation formulas and declarations. Below we describe the transformations considered: Reachability: When considering an initial quotient formula ? l0 not all identi?ers in DB may be reachf able. In Uppaal an “on-the-?y” technique insures that only the reachable part of DB is generated. Boolean Simpli?cation Formulas may be simpli?ed using the following simple boolean equations and their duals: ff ∧ ? ≡ ff, tt ∧ ? ≡ ?, a ff ≡ ff, ? ff ≡ ff, x in ff ≡ ff, a ? ∧ [a]ff ≡ ff. Constraint Propagation: Constraints on formula clocks may be propagated using various distribution laws (see Table 5). In some cases, propagation will lead to trivial clock constraints, which may be simpli?ed to either tt or ff and hence made applicable to Boolean Simpli?cation. Constant Propagation: Identi?ers with identi?erfree de?nitions (i.e. constants such as tt or ff) may be removed while substituting their de?nitions in the declaration of all other identi?ers. Trivial Equation Elimination: Equations of the def form X = [a]X are easily seen to have X = tt as solution and may thus be removed. More generally, let S be the largest set of identi?ers such that whenever def X ∈ S and X = ? then ?[tt/S ]6 can be simpli?ed to tt. Then all identi?ers of S can be removed provided the value tt is propagated to all uses of identi?ers from S (as under Constant Propagation). The maximal set S

6 ?[tt/S ] is the formula obtained by substituting all occurrences of identi?ers from S in ? with the formula tt.

Example 5 Reconsider the network and synchronization function from Examples 1, 2 and 3. We want to establish that the network Am |f Bn satis?es the following property Y provided n + m ≥ i: Y X

def

= =

[a] z in X (z ≥ i) ∨ [c]ff ∧ [a]X ∧ [b]X ∧ ? ?X

def

The property Y expresses that the accumulated time between an initial a-action and a following c-action must exceed i. We want to show that Cm,n satis?es this property provided the sum of the delays m and n exceeds the required delay i. That is, we must show [l0 , D0 ] [a](z in X ) provided n + m ≥ i. From Theorem 3 it follows that the su?cient and necessary requirement to Am in order that Am |f Bn satis?es Y is that Am satis?es Y k0 . Using the quof tient de?nition from Table 4 we get: Y X X

f

k0 k0 k1

def

= = =

z in (X

f

k0 )

f

def def

f

(z ≥ i) ∨ [b](y in X

k1 ) ∧ ? ?(X

f

k0 ) k1 )

f

(z ≥ i) ∨ (y ≥ n ? [c]ff) ∧ ? ?(X

f

2

5.2 Minimizations

It is obvious that repeated quotienting leads to an explosion in the formula. The crucial observation made by Andersen in the (untimed) ?nite-state case is that simple and e?ective transformations of the formulas in practice may lead to signi?cant reductions. In presence of real-time we need, in addition to the minimization strategies of Andersen, heuristics for propagating and eliminating constraints on clocks in 9

may be e?ciently computed using standard ?xed point computation algorithms. Equivalence Reduction: If two identi?ers X and Y are semantically equivalent (i.e. are satis?ed by the same timed transition systems) we may collapse them into a single identi?er and thus obtain reduction. However, semantical equivalence is computationally very hard7 . To obtain a cost e?ective strategy we approximate semantical equivalence of identi?ers as follows: Let R be an equivalence relation on identi?ers. R may be extended homomorphically to formulas in the obvious manner: i.e. (?1 ∧ ?2 )R(?1 ∧ ?2 ) if ?1 R?1 and ?2 R?2 , (x in ?)R(x in ?) and [a]?R[a]? if ?R? and so on. Now let ? = be the maximal equivalence relation on def identi?ers such that whenever X ? = Y , X = ? and def Y = ? then ? ? = ?. Then ? = provides the desired cost e?ective approximation: whenever X ? = Y then X and Y are indeed semantically equivalent. Moreover, ? = may be e?ciently computed using standard ?xed point computation algorithms. In the following Examples we apply the above transformation strategies to the quotient formula obtained in Example 5. In particular, the strategies will ?nd the quotient formula to be trivially true in certain cases. Example 6 Reconsider Example 5 with Y0 , X0 and X1 abbreviating Y k0 , X k0 and X k1 . Now Y0 f f f is the su?cient and necessary requirement to Am in order that Am |f Bn satis?es Y . From the de?nition of satis?ability for timed automata we see that: Am |= Y0 if and only if Am |= tt ? y in Y0

(D0 ? X0 ) (D0 ↑ ? X0 ) (D1 ? X1 ) (D0 ? X1 ) (D0 ↑ ? X1 )

≡ [b] y in (D0 ? X1 ) ∧ ? ? D0 ↑ ? X0 ≡ [b] y in (D1 ? X1 ) ∧ ? ? D0 ↑ ? X0 ≡ ≡ ≡ (D1 ∧ y ≥ n) ? [c]ff ∧ ? ?(D1 ↑ ? X1 ) (D0 ∧ y ≥ n) ? [c]ff ∧ ? ?(D0 ↑ ? X1 ) (D0 ↑ ∧ z < i ∧ y ≥ n) ? [c]ff ∧ ? ?((D0 ↑ ∧ z < i) ? X1 )

↑

(D1 ↑ ? X1 )

≡

(D1 ↑ ∧ z < i ∧ y ≥ n) ? [c]ff ∧ ? ?((D1 ↑ ∧ z < i) ? X1 )

↑

Table 6: Equations after Constraint Propagation Continuing constraint propagation yields the equations 2 in Table 6, where D1 = (y = 0 ∧ z < i). Example 7 (Example 6 Continued) Now consider the case when n ≥ i. That is the delay n of the component Bn exceeds the delay i required as a minimum by the property Y . Thus the component Bn ensures on its own the satis?ability of Y ; i.e. for any choice of A the system A |f Bn will satisfy Y . In this particular case (i.e. n ≥ i) it is easy to see that (Di ↑ ∧z < i∧y ≥ n) = ff for i = 0, 1 as Di ↑ ensures z ≥ y . Also for i = 0, 1, (Di ∧ y ≥ n) = ff as Di ? y = 0 and we assume n > 0. ↑ Finally, it is easily seen that (Di ↑ ∧ z < i) = Di ↑ for i = 0, 1. Inserting these observations — which all may be e?ciently computed — in the equations of Table 6 we get equations which after application of Boolean Simpli?cation and Trivial Equation Elimination all simpli?es to tt. Thus, in the case n ≥ i, our minimization heuristics will yield tt as the property required of A in order that 2 A |f Bn satis?es Y .

This provides an initial basis for constraint propagation. Using the propagation laws from Table 5 we get: tt ? y in Y0 ≡ tt ? {y, z } in X0 ≡ {y, z } in D0 ? X0 where D0 = (y = 0 ∧ z = 0). This makes the implication D0 ? X0 applicable to constraint propagation as follows: (D0 ? X0 ) ?X0 ≡ D0 ? (z ≥ i) ∨ [b](y in X1 ) ∧ ? ≡ D0 ? [b](y in X1 ) ∧ D0 ? ? ?X0

8

6

Experimental Results

≡ [b] y in (D0 ? X1 ) ∧ ? ? D0 ↑ ? X0

7 For

The techniques presented in previous sections have been implemented in our veri?cation tool Uppaal in C++ . We have tested Uppaal by various examples. We

8 Note

the full logic T? the equivalence problem is undecidable.

that (z < i ∧ D0 ) = D0 .

10

also perform experiments on three existing real-time veri?cation tools: HyTech (Cornell), Kronos (Grenoble), and Epsilon (Aalborg). Though the compositional model-checking technique is still under implementation, our experimental results show that Uppaal is not only faster than the other tools but also able to handle larger systems. In particular, we have used the so called Fischer’s mutual exclusion protocol [17, 18, 19] in our experiments on the tools. The reason for choosing this example is that it is well-known and well-studied by researchers in the context of real-time veri?cation. More importantly, the size of the example can be easily scaled up by simply increasing the number of processes in the protocol, thus increasing the number of control-nodes — causing state-space explosion — and the number of clocks — causing region-space explosion.

250 HyTech (verification) HyTech (total) Epsilon Kronos (verification) Kronos (total) UPPAAL

200

150

100

50

0 2 3 4 5 6 7

Figure 3: Execution Times. not only time but also (more importantly) space. For HyTech and Kronos we have measured both the total time as well as the part spent on the actual veri?cation i.e. not measuring the time for producing the product automaton.

6.1

Performance Evaluation

Using the current version of our tool Uppaal, installed on a SparcStation 10 running SunOS 4.1.2 with 64MB of primary memory and 64MB of swap memory, we have veri?ed the mutual exclusion property of Fischer’s protocol for the cases9 n = 2, . . . , 8. The time-performance of this experiment can be found in Figure 3. Execution times have been measured in seconds with the standard UNIX program time. We have also attempted to verify Fischer’s protocol using three other existing real-time veri?cation tools: HyTech [20] (version 0.6 and version 1.0), Kronos 1.1c [21] and Epsilon 3.0 [22] using the same machine as for the Uppaal experiment. As illustrated in Figure 3 the experiment showed that Uppaal is faster than all these tools and able to deal with larger systems; all the other tools failed10 to verify Fischer’s protocol for more than 5 processes. The four tools can be devided into two categories: HyTech and Kronos both produce the product of the automata network before the veri?cation is carried out, whereas Epsilon and Uppaal veri?es properties on-the?y without ever explicitly producing the product automaton (recently another on-the-?y veri?cation technique for timed automata has been studied in [23]). A potential advantage of the ?rst strategy is the reusability of the product automaton. The obvious advantage of the second strategy is that only the necessary part of product automaton needs to be examined saving

9 In fact we have veri?ed the case of 9 processes, but on a di?erent machine. 10 Failure occured either because the veri?cation ran out of memory, never terminated or did not accept the produced product automaton.

7

Conclusion and Future Work

In developing automatic veri?cation algorithms for real-time systems, we need to deal with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables. To attack these explosion problems, we have developed and combined compositional and symbolic model-checking techniques. These techniques have been implemented in a new automatic veri?cation tool Uppaal. Experimental results show that Uppaal is not only faster than other realtime veri?cation tools but also able to handle larger systems. We should point out that the safety logic we designed in this paper enables the presented techniques to be implemented in a very e?cient way. Though the logic is less expressive than the full version of the timed ?-calculus T? , it is expressive enough to specify safety properties as well as bounded liveness properties. As future work, we shall study the practical applicability of this logic and Uppaal by further examples. Our experience shows that the practical limits of Uppaal is caused by the space-complexity rather than the timecomplexity of the model-checking algorithms. Thus, future work includes development of more space-e?cient methods for representation and manipulation of clock 11

constraints. For a veri?cation tool to be of practical use in a design process it is of most importance that the tool o?ers some sort of diagnostic information in case of errors. Based on the synthesis technique presented in [24] we intend to extend Uppaal with the ability to generate diagnostic information. Finally, more sophisticated minimization heuristics are sought to yield further improvement of our compositional technique.

[10] H. R. Andersen. Partial Model Checking. In Proc. of LICS’95, 1995. [11] Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Veri?cation of Real-Time Systems By Constraint-Solving. In the Proceedings of the 7th International Conference on Formal Description Techniques, 1994. [12] F. Laroussinie and K.G. Larsen. Compositional Model Checking of Real Time Systems. Lecture Notes in Computer Science, 1995. Proc. of CONCUR’95. [13] H. H¨ uttel and K. G. Larsen. The use of static constructs in a modal process logic. Lecture Notes in Computer Science, Springer Verlag, 363, 1989. [14] Nicolas Halbwachs. Delay Analysis in Synchronous Programs. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV’93. [15] F. Laroussinie and K.G. Larsen. From Timed Automata to Logic — and Back. Lecture Notes in Computer Sciencie, 1995. Proc. of MFCS’95. [16] A. Tarski. A lattice-theoretical ?xpoint theorem and its applications. Paci?c Journal of Math., 5, 1955. [17] Kim G. Larsen, Paul Pettersson, and Wang Yi. Modelchecking for real-time systems. In Proc. of Fundamentals of Computation Theory, 1995. [18] Martin Abadi and Leslie Lamport. An Old-Fashioned Recipe for Real Time. Lecture Notes in Computer Science, 600, 1993. [19] N. Shankar. Veri?cation of Real-Time Systems Using PVS. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV’93. [20] Thomas A. Henzinger and Pei-Hsin Ho. HyTech: The Cornell HYbrid TECHnology Tool. Proc. of TACAS, Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995. BRICS report series NS–95–2. [21] C. Daws, A. Olivero, and S. Yovine. Verifying ETLOTOS programs with KRONOS. In Proceedings of 7th International Conference on Formal Description Techniques, 1994. [22] K. Cerans, J. C. Godskesen, and K. G. Larsen. Timed modal speci?cations — theory and tools. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV’93. [23] Oleg V. Sokolsky and Scott A. Smolka. Local model checking for real-time systems. In Proc. of CAV’95, volume 939, pages 211–224. Springer Verlag, 1995. [24] J.C. Godskesen and K.G. Larsen. Synthesizing Distinghuishing Formulae for Real Time Systems — Extended Abstract. Lecture Notes in Computer Science, 1995. Proc. of MFCS’95.

Acknowledgment

The Uppaal tool has been implemented in large parts by Johan Bengtsson and Fredrik Larsson. The authors would like to thank them for their excellent work. The ?rst author would also like to thank Francois Laroussinie for several interesting discussions on the subject of compositional model-checking. The last two authors want to thank the Steering Committee members of NUTEK, Bengt Asker and Ulf Olsson, for useful feedback on practical issues.

References

[1] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1020 states and beyond. Logic in Computer Science, 1990. [2] P. Godefroid and P. Wolper. A Partial Approach to Model Checking. Logic in Computer Science, 1991. [3] A. Valmari. A Stubborn Attack on State Explosion. Theoretical Computer Science, 3, 1990. [4] E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetry in Temporal Logic Model Checking. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV’93. [5] E. M. Clarke, O. Gr¨ umberg, and D. E. Long. Model Checking and Abstraction. Principles of Programming Languages, 1992. [6] E. A. Emerson and C. S. Jutla. Symmetry and Model Checking. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV’93. [7] R. Alur and D. Dill. Automata for Modelling Real-Time Systems. Theoretical Computer Science, 126(2):183–236, April 1994. [8] R. Alur, C. Courcoubetis, and D. Dill. Model-checking for Real-Time Systems. In Proceedings of Logic in Computer Science, pages 414–425. IEEE Computer Society Press, 1990. [9] T. A. Henzinger, Z. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Logic in Computer Science, 1992.

12

Recent Publications in the BRICS Report Series

RS-96-59 Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. December 1996. 12 pp. Appears in 16th IEEE Real-Time Systems Symposium, RTSS ’95 Proceedings, 1995. RS-96-58 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal — a Tool Suite for Automatic Veri?cation of Real–Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS Workshop on Veri?cation and Control of Hybrid Systems, HYBRID ’96 Proceedings, LNCS 1066, 1996, pages 232–243. RS-96-57 Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS Workshop on Veri?cation and Control of Hybrid Systems, HYBRID ’96 Proceedings, LNCS 1066, 1996, pages 575–586. RS-96-56 Zine-El-Abidine Benaissa, Pierre Lescanne, and Kristoffer H. Rose. Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution. December 1996. 35 pp. Appears in Kuchen and Swierstra, editors, 8th International Symposium on Programming Languages, Implementations, Logics, and Programs, PLILP ’96 Proceedings, LNCS 1140, 1996, pages 393–407. RS-96-55 K? are J. Kristoffersen, Franc ? ois Laroussinie, Kim G. Larsen, Paul Pettersson, and Wang Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. December 1996. 14 pp. To appear in Dauchet and Bidoit, editors, Theory and Practice of Software Development. 7th International Joint Conference CAAP/FASE, TAPSOFT ’97 Proceedings, LNCS, 1997. RS-96-54 Igor Walukiewicz. Pushdown Processes: Games and Model Checking. December 1996. 31 pp. Appears in Alur and Henzinger, editors, 8th International Conference on Computer-Aided Veri?cation, CAV ’96 Proceedings, LNCS 1102, 1996, pages 62–74.

- Symbolic model checking of real-time systems
- CMC A Tool for Compositional Model-Checking of Real-Time Systems
- Forward and Time-Jumping Symbolic Model Checking for Real Time Systems
- Symbolic Model Checking for Real-Time Systems
- Model checking real-time properties of symmetric systems
- Model-checking for real-time systems
- How to Verify a Safe Real-Time System. The Application of Model Checking and a Timed Automa
- Monitoring, checking, and steering of real-time systems
- Collaborative model and algorithms for supporting real-time distribution logistics systems
- Model checking probabilistic real time systems

更多相关文章：
**
***Model* *Checking*(Part 1)_图文.ppt

*Symbolic* *Model* *Checking* 7. *Model* *Checking* for the...12.*Compositional* Reasoning 13.Abstraction 14....*Systems* 16.Discrete *Real-Time* & Quantitative ...**
一种基于满足性判定的并发软件验证策略.pdf
**

江苏镇江212013) SAT-Based*Compositional*Verification...aframeworkfor*modelchecking*concurrent software*systems*...*and*the*modelchecking*stepis*symbolic*.Exampleshowsthatthe...**
***Compositional* *and* *Symbolic* *Model-Checking* *of* *Real-Time* *Systems*.unkown

*Compositional* *and* *Symbolic* *Model-Checking* *of* *Real-Time* *Systems* Kim G. Larseny Paul Petterssonz Wang Yiz Uppsala University Abstract E cient automatic model...**
***Symbolic* *Model* *Checking* *of* *Real-Time* *Systems*.unkown

*Symbolic* *Model* *Checking* *of* *Real-Time* *Systems* G. Logothetis *and* K. Schneider University *of* Karlsruhe Institute for Computer Design *and* Fault Tolerance (Prof....**
***Symbolic* *Model* *Checking* for *Real-time* *Systems*.unkown

*Symbolic* *Model* *Checking* for *Real-time* *Systems* Thomas A. Henzingery Computer Science Department, Cornell University Ithaca, NY 14853, U.S.A. Xavier Nicoll...**
***Symbolic* *Model* *Checking* *of* *Real-Time* *Systems* using Difference....unkown

Summary*of* results *Symbolic* *Model* *Checking* *of* *Real-Time* *Systems* using Difference Decision Diagrams p.2/38 Background x More *and* more *systems* contain ...**
***Symbolic* *Model* *Checking* *of* *Real-Time* *Systems*.unkown

*Symbolic* *Model* *Checking* *of* *Real-Time* *Systems* G .Logothetis *and* K. Schneider University *of* Karlsruhe Institute for Computer Design *and* Fault Tolerance (Prof....**
On-the-Fly ***Symbolic* *Model* *Checking* for *Real-Time* *Systems* *.unkown

On-the-Fly*Symbolic* *Model* *Checking* for *Real-Time* *Systems* * Ahmed Bouajjani Stavros Tripakis Sergio Yovine VERIMAG Centre Equation, 2 av. de Vignate, ...**
...Embedded ***Real-Time* *Systems* Using *Symbolic* *Model* *Checking*: ....unkown

*Real-Time* *Systems* Using *Symbolic* *Model* *Checking*: A Case Study Tao Pang, ... abstract *model* *checking* (AMC) [15], *and* *compositional* *model* *checking* (CMC...**
...***Model* *Checking* for Complete *and* Incomplete *Real-Time* *Systems*.unkown

Board*of* SFB/TR 14 AVACS Fully *Symbolic* TCTL *Model* *Checking* for Complete *and* Incomplete *Real-Time* *Systems* by Georges Morbe *and* Christoph Scholl AV...**
Forward ***and* *Time*-Jumping *Symbolic* *Model* *Checking* for *Real* ....unkown

Forward*and* *Time*-Jumping *Symbolic* *Model* *Checking* for *Real* *Time* *Systems* Georgios Logothetis University *of* Karlsruhe Department *of* Computer Science Institute for ...**
On-the-Fly ***Symbolic* *Model* *Checking* for *Real-Time* *Systems* y.unkown

On-the-Fly*Symbolic* *Model* *Checking* for *Real-Time* *Systems* y Ahmed Bouajjani Stavros Tripakis Sergio Yovine VERIMAG Centre E quation, 2 av. de ...**
***Compositional* *Model* *Checking* *of* *Real* *Time* *Systems*.unkown

BRICS Basic Research in Computer Science*Compositional* *Model* *Checking* *of* *Real* *Time* *Systems* Francois Laroussinie Kim G. Larsen BRICS Report Series ISSN ...**
...***checking* for complete *and* incomplete *real-time* *systems* ....unkown

*symbolic* TCTL *model* *checking* for complete *and* incomplete *real-time* *systems* , Georges Morbé , Christoph Scholl Department *of* Computer ...**
...***model* *checking* for *timing* analysis *of* Java *real-time* *systems*.unkown

10.1186/s13639-015-0020-8 RESEARCH Open Access*Symbolic* execution *and* timed automata *model* *checking* for timing analysis *of* Java *real-time* *systems* Kasper ...**
科学文献.pdf
**

Yi.*Compositional* *and* *Symbolic* *Model-Checking* *of* *Real-Time* *Systems*. To appear in Proc. *of* the 16th IEEE *Real-Time* *Systems* Symposium, December 1995. LPY...**
***Symbolic* *Model* *Checking* for Event- Driven *Real-Time* *Systems*.unkown

*real-time* verification, *symbolic* *model* *checking*, synchronous *real-time* event logic This article was supported in part by a research grant from the Office...**
Forward ***Symbolic* *Model* *Checking* for *Real* *Time* *Systems*.unkown

Forward*Symbolic* *Model* *Checking* for *Real* *Time* *Systems* PII-3 Georgios Logothetis University *of* Karlsruhe Institute for Computer Design *and* Fault Tolerance ...**
科学文献.pdf
**

*Compositional* *and* *SymbolicModel-Checking* *of* *Real-Time* *Systems*. In Proc. *of* the 16th IEEE *Real-Time* *Systems* Symposium, pages 76{87, December 1995. 10] ...**
***Symbolic* *Model* *Checking* for *Real**Time* *Systems**.unkown

INFORMATION*AND* COMPUTATlON 111, 193-244 (1994) *Symbolic* *Model* *Checking* for *Real**Time* *Systems** THOMAS A. HENZINGEIU Computer Science Department, Cornell ... 更多相关标签：

江苏镇江212013) SAT-Based

Summary

On-the-Fly

Board

Forward

On-the-Fly

BRICS Basic Research in Computer Science

10.1186/s13639-015-0020-8 RESEARCH Open Access

Yi.

Forward

INFORMATION