Model checking and modular verification.
We describe a framework for compositional verification of finite-state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition, and a preorder on structures which captures the relation between a component and a system containing the component. Satisfaction of a formula in the logic corresponds to being below a particular structure (a tableau for the formula) in the preorder. We show how to do assume-guarantee-style reasoning within this framework. Additionally, we demonstrate efficient methods for model checking in the logic and for checking the preorder in several special cases. We have implemented a system based on these methods, and we use it to give a compositional verification of a CPU controller.
Introduction
Temporal logic model checking procedures are useful tools for the verification of finite state
systems [3, 12, 20]. However, these procedures have traditionally suffered from the state
explosion problem. This problem arises in systems which are composed of many parallel
processes; in general, the size of the state space grows exponentially with the number of
processes. By introducing symbolic representations for sets of states and transition relations
and using a symbolic model checking procedure, systems with very large state spaces (10 100
or more states) can be verified [1, 8]. Further, the time and space requirements with these
techniques may in practice be polynomial in the number of components of the system.
This research was sponsored in part by the Avionics Laboratory, Wright Research and Development
Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, Ohio 45433-6543
under Contract F33615-90-C-1465, ARPA Order No. 7597 and in part by the National Science Foundation
under Contract No. CCR-9005992 and in part by the U.S.-Israeli Binational Science Foundation.
The views and conclusions contained in this document are those of the authors and should not be interpreted
as representing the official policies, either expressed or implied, of the U.S. government.
Unfortunately, the symbolic procedures still have limits, and many realistic problems are
not tractable due to their size. Thus, we are motivated to search for additional methods
of handling the state explosion problem, methods which work well in conjunction with the
techniques.
An obvious method for trying to avoid the state explosion problem is to use the natural
decomposition of the system. The goal is to verify properties of individual components,
infer that these hold in the complete system, and use them to deduce additional properties
of the system. When verifying properties of the components, it may also be necessary to
make assumptions about the environment. This approach is exemplified by Pnueli's assume-guarantee
paradigm [23]. A formula in his logic is a triple h'iM h/i where ' and / are
temporal formulas and M is a program. The formula is true if whenever M is part of a
system satisfying ', the system must also satisfy /. A typical proof shows that h'iM h/i
and htrueiM 0
hold and concludes that htrueiM k M 0
h/i is true.
In order to automate this approach, a model checker must have several properties. It
must be able to check that a property is true of all systems which can be built using a given
component. More generally, it must be able to restrict to a given class of environments when
doing this check. It must also provide facilities for performing temporal reasoning. Most
existing model checkers were not designed to provide these facilities. Instead, they typically
assume that they are given complete systems.
An elegant way to obtain a system with the above properties is to provide a preorder on
the finite state models that captures the notion of "more behaviors" and to use a logic whose
semantics relate to the preorder. The preorder should preserve satisfaction of formulas of
the logic, i.e., if a formula is true for a model, it should also be true for any model which is
smaller in the preorder. In addition, composition should preserve the preorder, and a system
should be smaller in the preorder than its individual components. Finally, satisfaction of
a formula should correspond to being smaller than a particular model (a tableau for the
formula) in the preorder. In such a framework, the above reasoning sequence might be
expressed as: T is the tableau of ', M k T
assumptions may be given either as formulas or directly as finite state models, whichever is
more concise or convenient. More complex forms of reasoning such as induction [18] are also
possible within this framework.
In choosing a computational model, a logic and a preorder to obtain a system such as
this, we are guided by the following considerations. First, we must be able to realistically
model physical systems such as circuits. Second, there should be efficient procedures for
model checking and for checking the preorder. Finally, it should be possible to implement
these procedures effectively using symbolic techniques.
In this paper, we propose a preorder for use with a subset of the logic CTL* [11]. This
subset is strictly more expressive than LTL. Further, the induced subset of CTL is expressive
enough for most verification tasks and has an efficient model checking algorithm. We also
give a tableau construction for this CTL subset. The construction provides a means of
temporal reasoning and makes it possible to use formulas as assumptions. Our preorder and
the semantics of our logics both include a notion of fairness. This is essential for modeling
systems such as communication protocols. We show how to use our results to verify systems
composed of Moore machines. Moore machines have an explicit notion of input and output
and are particularly suitable for modeling synchronous circuits. Finally, we suggest efficient
methods for checking the preorder in several interesting cases. We have implemented a
system based on these results; the system supports efficient compositional verification and
temporal reasoning.
Our paper is organized as follows. Section 2 surveys some related work. In section 3,
we present the logic and its semantics (for Kripke structures). The preorder and some of
its properties are given in section 4. The next section defines the semantics of the logic for
Moore machines. Given a Moore machine and a formula, we show how to efficiently check
whether for all environments, the Moore machine in the environment satisfies the formula.
Section 6 presents the tableau construction and demonstrates how to use it for temporal
reasoning. Methods for checking the preorder are discussed in section 7. Section 8 gives a
compositional verification of a simple CPU controller. We conclude with a summary and
some directions for future work.
Related work
Much of the work on reducing the complexity of automatic verification can be grouped into
two classes. The first class includes methods to build a reduced global state graph or to
expand only the needed portion of the global state graph.
Local model checking algorithms [6, 26, 29] based on logics like the -calculus use a
tableau-based procedure to deduce that a specific state (the initial state of the system)
satisfies a given logical formula. The state space can be generated as needed in such an
algorithm, and for some formulas, only a small portion of the space may have to be examined.
The main drawback of these algorithms is that often the entire space is generated (for
example, when checking that a property holds globally). It is also not clear whether the
algorithms can take good advantage of symbolic representations.
Graf and Steffen [13] describe a method for generating a reduced version of the global
state space given a description of how the system is structured and specifications of how
the components interact. Clarke, Long and McMillan [4] describe a similar attempt. Both
methods will still produce large state graphs if most of the states in the system are not
equivalent, and much of the verification must be redone if part of the system changes.
Shtadler and Grumberg [24] show how to verify networks of processes whose structure is
described by grammars. In this approach, which involves finding the global behavior of each
component, networks of arbitrary complexity can be verified by checking one representative
system. For many systems, however, the number of states may still be prohibitive, and it is
not clear whether the method can use symbolic representations.
The second class of methods are compositional; properties of the individual components
are verified, and properties of the global system are deduced from these. A representation
of the global state space is not built.
Josko [15] gives an algorithm for checking whether a system satisfies a CTL specification
in all environments. His algorithm also allows assumptions about the environment to be
specified in a restricted linear-time logic. The system is able to handle assume-guarantee
reasoning. The method is fairly ad hoc however, and more complex forms of reasoning such
as induction cannot be easily incorporated into the system.
Within the framework of CCS [22], there have been a number of suggestions for compositional
reasoning. Larsen [19] investigates the expressive power of formalisms for specifying
the behavior of a process in a system. He suggests equivalence, refinement and satisfaction
(of a formula) as three interesting relations between an implementation and its specification.
However, he does not discuss the applicability of these ideas to verification, nor does he
suggest how they can be implemented. Walker [27] demonstrates how to use a preorder plus
knowledge of how a system should operate to simplify the verification of bisimulation equiv-
alence. Cleaveland and Steffen [7] use a similar idea. Winskel [28] proposes a method for
decomposing specifications into properties which the components of a system must satisfy
for the specification to hold. The approach is very appealing, but unfortunately, dealing
with parallel composition is difficult. It is not apparent whether any of these methods will
work well with symbolic representations.
Kurshan [16] describes a verification methodology based on testing containment of !-
regular languages. Homomorphic reductions are used to map implementations to specifica-
tions, and the specifications may be used as implementations at the next level of abstraction.
Dill [10] proposes an elegant form of trace theory which can be used in a similar manner,
but the framework does not handle liveness properties well. Both approaches depend on
specifications being deterministic for efficiency, and neither approach makes provisions for
using logical formulas as specifications or assumptions.
Shurek and Grumberg [25] describe criteria for obtaining a modular framework, and
illustrate the idea using CTL* with only universal path quantifiers. This system is closest to
the work presented here, but they give no provisions for handling fairness efficiently, using
formulas as assumptions, or supporting temporal reasoning. Models in their system are also
associated with a fixed decomposition into components; hence it is unclear how to perform
inductive reasoning in the framework.
3 Temporal logic
The logics presented in this section are branching-time temporal logics. In order to be able
to efficiently decide whether a formula is true in all systems containing a given component,
we eliminate the existential path quantifier from the logics. Thus, a formula may include
only the universal quantifier over paths, but unlike in linear-time temporal logic, nesting
of path quantifiers is allowed. To ensure that existential path quantifiers do not arise via
negation, we will assume that formulas are expressed in negation normal form. In other
words, negations are applied only to atomic propositions. The logics are interpreted over a
form of Kripke structure with fairness constraints. Path quantifiers range over the fair paths
in the structures.
The logic 8CTL* is the set of state formulas given by the following
inductive definition.
1. The constants true and false are state formulas. For every atomic proposition p,
and :p are state formulas.
2. If ' and / are state formulas, then ' - / and ' - / are state formulas.
3. If ' is a path formula, then 8(') is a state formula.
4. If ' is a state formula, then ' is a path formula.
5. If ' and / are path formulas, then so are ' - /.
6. If ' and / are path formulas, then so are
(a) X ',
(b) ' U /, and
We also use the following abbreviations: F ' and G ', where ' is a path formula, denote
(true U ') and (false V ') respectively.
8CTL is a restricted subset of 8CTL* in which the 8 path quantifier may only precede
a restricted set of path formulas. More precisely, 8CTL is the logic obtained by eliminating
rules 3 through 6 above and adding the following rule.
3'. If ' and / are state formulas, then 8X', 8(' U /), and 8(' V /) are state formulas.
In practice, we have found that many of the formulas which are used in specifying and
verifying systems are expressible in 8CTL, and almost all are expressible in 8CTL*. An
example formula which is not expressible in 8CTL* is a weak form of absence of deadlock:
states that it should always be possible to reach a state where p holds.
We will give the semantics of the logic using a form of Kripke structure with fairness
constraints.
is a tuple of the following
form.
1. S is a finite set of states.
2. S 0 ' S is a set of initial states.
3. A is a finite set of atomic propositions.
4. L is a function that maps each state to the set of atomic propositions true in that state.
5. R ' S \Theta S is a transition relation.
6. F is a Streett acceptance condition, represented by pairs of sets of states.
Definition 3 A path in M is an infinite sequence of states . such that for all
for infinitely many i g. - is a fair path in M iff
for every
The notation - n will denote the suffix of - which begins at s n . We now consider the
semantics of the logic 8CTL* with atomic propositions drawn from the set A.
Definition 5 (satisfaction of a formula) Satisfaction of a state formula ' by a state s
and of a path formula / by a fair path - j= /) is defined inductively as follows.
1. s
2. s
3. s for every fair path - starting at s, -
4. - is a state formula, iff the first state of - satisfies the state formula.
5. -
6. (a) -
(c) -
indicates that for every s 0
Emerson and Halpern [11] compared the expressive power of the three logics LTL, CTL
and CTL*. They showed that LTL and CTL have incomparable expressive power, while
CTL* is strictly more expressive than either of the others. Eliminating the existential path
quantifier from CTL and CTL* does not affect the relative expressive power of the logics.
8CTL* trivially encompasses LTL and 8CTL. The formula 8F8Gp is a formula of 8CTL
that does not have an equivalent LTL formula. On the other hand, there is no
that is equivalent to the LTL formula 8FG p. Thus, LTL and 8CTL are incomparable, and
both are strictly less expressive than 8CTL*.
4 Homomorphisms and composition of structures
In this section, we define the preorder which we use and examine some of its properties. We
also show how these properties make assume-guarantee style reasoning possible.
Definition 6 (structure homomorphism) Let M and M 0 be two structures with A ' A 0 ,
and let t and t 0 be states in S and S 0 , respectively. A relation H ' S \Theta S 0 is a homomorphism
from (M; t) to (M the following conditions hold.
1. H(t; t 0 ).
2. For all s and s 0 , H(s; s 0 ) implies
(a)
(b) for every fair path in M there exists a fair path -
1 . from s
in M 0 such that for every
When H satisfies property 2, we say H is a homomorphism. H is a homomorphism from M
to M 0 iff for every s 0 2 S 0 there is s 0
0 such that H(s
To indicate that two paths
correspond as in item 2b above, we write H(- 0 ).
there is a homomorphism from
(M; s) to (M there exists a homomorphism from M to M 0 .
When M and M 0 are understood, we sometimes write s - s 0 . Intuitively, two states
are homomorphic if their labels agree on the atomic propositions of the second structure
and if for every fair path from the first state there is a corresponding fair path from the
second state. Two structures are homomorphic if for every initial state of the first, there
is a corresponding initial state of the second. One may view the second structure as a
specification and the first as its implementation. Since a specification may hide some of the
implementation details, it may have a smaller set of atomic propositions.
Definition 8 (composition of structures) Let M and M 0 be two structures. The composition
of M and M 0 , denoted M k M 0 , is the structure M 00 defined as follows.
1.
2. S 00
3. A
4. L 00
5. R 00
The choice of this definition of composition is motivated by its correspondence with
composition of Moore machines. Each transition of the composition is a joint transition of
the components, and states of the composition are pairs of component states that agree on
their common atomic propositions. We first note that this composition operator has the
usual properties.
Theorem 1 Composition of structures is commutative and associative (up to isomorphism).
Proof Straightforward but tedious. 2
We now turn to the connections between the relation - and composition. To begin, we
note that a path in M k M 0 is fair iff its restriction to each component results in a fair path.
. The following conditions are equivalent.
1.
. is a fair path in M 00 .
2.
1 . are fair paths in M and M 0 respectively, and (s
) is a
state of M 00 for all i 2 N.
Proof Assume condition 1 above. By the definition of composition, . is a path
in M . Let
;. By the definition of a fair path, inf(- 00
Hence so - is a fair path in M . Similarly, -
1 . is a fair path
in M 0 .
Assume condition 2 above. From the definition of composition, -
a path in M 00 . Suppose
(P \Theta S 0
for some
for
some . In the first case, we have
implies
;. The second case is similar. Hence - 00 is a fair path in M 00 . 2
Theorem 2
1. - is a preorder.
2. For all M and M 0 ,
- M .
3. For all
4. For all M , M - M k M .
Proof
1. The relation
(s; s)
is a homomorphism from M to M , so - is reflexive.
Thus it only remains to show that - is transitive. Assume
Let H 0 be a homomorphism from M to M 0 , and let H 1 be a homomorphism from M 0
to M 00 . Define H 2 as the relational product of H 0 and H 1 , i.e.,
then by the definition of homomorphism, there exists s 0
0 such
that H 0
Similarly, there exists s 00
0 such that H 1 (s 0
be such that H 0 (s; s 0 ) and H 1 By the definition
of homomorphism,
we have is a fair path in M from s, then there exists a fair
path - 0 from s 0 in M 0 such that H 0 (- 0 ). Since H 1 is a homomorphism, there exists
a fair path - 00 from s 00 in M 00 such that H 1 (-
is a homomorphism from M to M 00 . Thus M - M 00 .
2. Define H by
is an initial state of M kM 0 , then s 0 . The label of (s; s 0 ) is L(s)[L 0 (s 0 ),
and
. is a fair path in M k M 0 , then by
the previous lemma, s 0 s 1 . is a fair path in M . By the definition of H , H
for every i. Hence H is a homomorphism and M k M 0 - M .
3. Let H 0 be a homomorphism from M to M 0 . Define H 1 by
ni
We show that H 1 is a homomorphism. Let (s
be an initial state of M k M 00 . By
the definition of composition, s 0
0such that H 0
0 ) is a state of M 0 k M 00 since
Further,
is an initial state of M 0 k M 00 by the definition of composition. By
definition of H 1 , we have H 1
. First note that
. be a fair path in M k M 00 from (s; s 00
every
A. By the previous lemma,
a fair path in M starting at s, and -
1 . is a fair path in M 00 from s 00 . Since
there is a path -
1 . from s
in M 0 such that for every i 2 N,
By the definition of homomorphism, L(s
Arguing
as above, we then have
for each i, and so each (s 0
a state in M 0 k M 00 . Now H 1
by the definition of H 1 . Applying the
previous lemma, we find that (s 0
. is a fair path starting in (s
corresponding to the path (s
4. First note that for every state s of M , (s; s) is a state of M k M . Define
. If s 0 2 S 0 , then by the definition of composition, (s is an
initial state of M k M . (s; s) trivially has the same label as s. Using the previous
lemma and the definition of composition, we find that if s 0 s 1 . is a fair path in M ,
then . is a fair path in M k M . By the definition of H, we have
for all i. Hence H is a homomorphism and M - M k M . 2
Theorem 3 Let s and s 0 be states of M and M 0 , and let H be a homomorphism such that
paths such that H(- 0 ). Then
1. for every 8CTL* (state) formula ' (with all atomic propositions in A 0
2. for every 8CTL* path formula ' (with all atomic propositions in A 0
Proof The proof proceeds by induction on the structure of the formula.
1. If false , the result is trivial. If an atomic proposition, then
By the definition of homomorphism, L(s)"A
and so '. The case where
2. If . The induction hypothesis implies
s '. The case where
3. If for every fair path - from s, - any fair path
from s. By the definition of homomorphism, there exists a fair path - 0 from s 0 such
that H(- 0 ). If s 0 - 0 from s 0 . The induction hypothesis
then implies -
4. If ' is a path formula consisting of only a state formula and - 0 then the initial
state s 0 of - 0 satisfies '. By the induction hypothesis, s since s is the initial
state of -
5. The cases for the conjunction and disjunction of path formulas are similar to case 2.
6. (a) If Now since H(- 0 ), we also have
the induction hypothesis implies - 1
(b) If implies there exists n such that - 0n
j. Applying the
induction hypothesis, - n
(c) The case where is similar to the previous two cases. 2
Corollary . Then for every 8CTL* formula ' (with atomic propositions
in A 0
Proof Immediate. 2
Using theorem 2 and this corollary, we see that a standard CTL (CTL*) model checking
algorithm [3], when restricted to 8CTL (8CTL*), can be viewed as determining whether
a formula is true of all systems containing a given component. This is the key to compositional
verification. With the theorem and corollary, it is also straightforward to justify
the soundness of the assume-guarantee paradigm when assumptions are given as structures.
(The connection between structures and formulas will be examined in section 6.) Discharging
an assumption involves checking for the relation -. Suppose that we wish to check that
and that we have verified the following relationships:
In other words, M discharges assumption A, M 0 under assumption A discharges assumption
A 0 , and M under assumption A 0 satisfies the desired formula. From theorem 2, we
have
Then corollary 1 implies that M k M 0 '. The theorem and corollary also show that
any system containing M k M 0 will satisfy '. Note that ' is not necessarily true in either
or M 0 and may involve atomic propositions from both M and M 0 .
5 Moore machines
We have seen that the structures defined earlier (definition 2) can be used for compositional
reasoning about synchronous systems. However, such systems are typically given using a
more common finite state model such as Moore machines [14]. Moore machines are models of
computation with an explicit notion of inputs and outputs. Since the inputs originate from an
external, uncontrolled environment, the machine can always receive any combination of input
values. Moore machines are synchronous; in a composition of Moore machines, each machine
makes a single step at every point. Thus, they are most suitable for modeling synchronous
circuits. In this section, we show a natural correspondence between Moore machines with
an empty set of inputs and the structures defined earlier. We use this correspondence to
define the semantics of 8CTL* with respect to Moore machines, and we show how to use
compositional reasoning to verify a system composed of Moore machines.
Definition 9 (Moore machine) A Moore machine is a tuple of
the following form
1. S is a finite set of states.
2. S 0 ' S is a set of initial states.
3. I is a finite set of input propositions.
4. O is a finite set of output propositions.
5. L is a function that maps each state to the set of output propositions true in that state.
I \Theta S is the transition relation.
We require that I " and that for every s 2 S and v ' I, there exists some t 2 S such
that R(s; v; t). We also let A denote I [ O.
(composition of Moore machines) Let M and M 0 be Moore machines
with O " O ;. The composition of M and M 0 , denoted M kM 0 , is the Moore machine M 00
defined as follows.
1.
2. S 00
3. I
4. O
5. L 00
and R 0
We now turn to the question of how to define satisfaction of a specification by a Moore
machine M . The key consideration is that we wish to have a compositional method of
reasoning. Thus, M satisfying a specification should mean that M plus any environment
satisfies that specification. We will achieve this by considering the behavior of complete
systems involving M .
Definition 11 A Moore machine M is called closed if I = ;.
Intuitively, the behavior of a closed machine cannot be altered. For such a machine, there
is a structure which naturally corresponds to it. We define this structure precisely now. The
definition here is actually slightly more general in that it assigns a structure to non-closed
machines as well.
Definition 12 (structure for a Moore machine) The structure M 0 corresponding to a
Moore machine M , denoted by K(M), is defined as follows.
1. I .
2. S 0
I .
3. A
4. L 0
(s; v)
5. R 0
Definition 13 A Moore machine M 0 is called a closing environment for M if O " O
I ' O 0 and I 0 ' O.
If M 0 is a closing environment for M , then M and M 0 can be composed, and the resulting
Moore machine will be closed. We now define satisfaction of a formula by a Moore machine.
Definition 14 (satisfaction in a Moore machine) If M is a Moore machine and ' is
a 8CTL* formula with atomic propositions over A, then M for every closing environment
We must now demonstrate how to efficiently check whether M
are Moore machines with O "O
to K(M) k K(M 0 ).
Proof Define OE mapping the states of K(M kM 0 ) to the states of K(M)kK(M 0 ) as follows.
OE
Suppose
and
both map to the same state of K(M) k K(M 0 ). Then
from the definition of OE, we immediately have
" I and
" I 0 . By the definition of Moore machine
composition, v and u are disjoint from O [O 0 . Hence This
implies Hence OE is an injection.
To argue that OE is surjective, we consider the cardinalities of the two sets of states. First,
we have
Now consider jS This is the number of states in the cross product S K(M) \Theta S K(M 0 )
which have compatible labelings. Fix a pair of states s and s 0 . There are 2 jI j states in K(M)
with s as their first component and 2 jI 0 j in K(M 0 ) with s 0 as the first component. Thus there
are potentially 2 jIj states in K(M corresponding to s and s 0 . However, each
must correspond on the atomic propositions in I " O 0 , I 0 " O, and I " I 0 . Thus there
are exactly
states in K(M) k K(M 0 ) corresponding to s and s 0 . Thus we have
Hence OE is a bijection.
If
is an initial state of K(M k M 0 ), then s 0
. Then
OE
is an initial state of K(M )kK(M 0 ) since s 0
is
an initial state of K(M ) and s 0
implies
is an initial state of K(M 0 ).
Similarly, if OE
is an initial state of K(M) k K(M 0 ), then
is an initial
state of K(M k M 0 ).
The sets of atomic propositions of the two structures are clearly identical. The labeling
of
is v. The labeling of OE
is
(v
(v
s; (v [L 0 (s
and
and R K(M
. The fairness sets
of both structures are empty. 2
Definition 15 If M is a Moore machine, the maximal closing environment for M , denoted
E(M), is the Moore machine M 0 defined as follows.
1.
2. S 0
3. I
4. O
5.
The maximal environment (for M) represents an environment which can do anything at
each step. Intuitively, a possible behavior of M in an arbitrary environment must also be a
possible behavior of M in the maximal environment. The logics we use specify properties
that should hold for every possible behavior of a system. Hence, if M plus its maximal
environment satisfies a formula, then M in any environment should satisfy that formula.
Lemma is a closing environment for M , and suppose M
Proof Define
Note that for every s 0 2 S 0 , there is some s 00 2 S 00 such that H(s the
state L 0
0 , there is s 00
0 which is related to it by H, and every
state in M 00 is an initial state.
If H(s by the definition of H , we have L 0
in M 0 , then the fact that every state in M 0 is related to some state in M 00 plus the fact that
R 00 is identically true implies that there is a path - 00 in M 00 such that H(-
every path in M 00 is fair. Thus H is a homomorphism. 2
Lemma 4 Let M be a Moore machine. Then K(M ) is isomorphic to K(M k E(M)).
mapping the states of M 00 to
the states of M 0 by OE
v). OE is obviously an injection, and OE is a surjection
since each subset of 2 I is a state of E(M ).
If
must be in S 0 . Hence
. Similarly, if (s
then
. A 00 and A 0 are trivially equal. We also have
(s; v)
(s; v)
Finally, we have R 00
. F 00 and F 0 are both empty. 2
Theorem 4 If M is a Moore machine, then M
Proof Suppose K(M) 4, we find K(M k E(M)) j= ', and then by
lemma 2, K(M) k K(E(M be any closing environment for M . By lemma 3,
Hence by theorem 2, K(M) k K(M 0 Applying
corollary 1, we have K(M) k K(M 0 )
to
If M hence by lemma 4, K(M)
Thus, to determine if a system M 1 k M 2 k . k M n satisfies a formula ', we instead check
that lemma 2, this is equivalent to checking that
the formula. As illustrated in the previous section,
we can use the assume-guarantee paradigm to try to verify this latter relation. Thus, during
an actual verification we will be working with structures even though the thing we want to
verify is a property of a composition of Moore machines.
6 The tableau construction
In this section, we give a tableau construction for 8CTL formulas (for a similar construction
for LTL, see Burch et al. [1]). We show that the tableau of a formula is a maximal model for
the formula under the relation -. Thus, the structure generated in the construction can be
used as an assumption by composing the structure with the desired system before applying
the model checking algorithm. Discharging the assumption is simply a matter of checking
that the environment satisfies the formula. We also indicate how the tableau can be used to
do temporal reasoning. For the remainder of this section, fix a 8CTL formula /.
Definition 16 The set sub(') of subformulas of the formula ' is defined by the following
equations.
1. If an atomic proposition, then f'g. If
negated atomic proposition, then pg.
2. If
3. (a) If
(b) If
(c) If
Definition 17 The set el(') of elementary formulas of the formula ' is defined by the
following equations.
1. If an atomic proposition, or
then fpg.
2. If
3. (a) If
(b) If
(c) If
The special elementary subformula 8X false denotes the nonexistence of a fair path;
s false indicates that no fair path begins at s.
Definition of a formula) The tableau of /, denoted T(/), is the structure
Fi defined as follows.
1.
2. is the map from el(/) [ sub(/) [ ftrue; falseg to S defined by the
following equations.
(a) g. If
then
(b) If
(c) i. If
ii. If
3. g.
4. g.
5. R(s; t) iff for each formula 8X' in el(/), 8X' 2 s implies t 2 \Phi(').
Lemma 5 For all subformulas ' of /, if s 2 \Phi('), then s
Proof The proof proceeds by induction on the structure of '.
1. If and every state satisfies true. If
so the result is trivial. If an atomic proposition, then g.
negated atomic
proposition, then g. Since we have that
2. If
the induction hypothesis, s . The case
3. (a) If
R(s; t). By the definition of R, we have t 2 \Phi(' 1 ), and then the induction
hypothesis implies t chosen arbitrarily, any fair path from s
satisfies ' 1 at its second state, and hence s
(b) If
t be any state in \Phi('). Then either
case t has no successors and t trivially, or
which case the induction hypothesis implies t
'). In this case, the induction hypothesis implies t
By the definition of R, we also know that if R(t; u), then u 2 \Phi(').
consider a fair path . from s. Note that no state on
this path can satisfy the first condition above. There are two cases to consider.
i. There is some j such that s j be the first such state on the path.
By the above, for every Hence the path satisfies ' 1 U ' 2 .
ii. For every j, s j 6j= ' 2 . Then the above implies that for every j, s
By the induction hypothesis, we know that each s j is not in \Phi(' 2 ). But then
By the definition of F, this
contradicts the fact that - is fair, and so this case is impossible.
Thus s
(c) If
t is any state in \Phi('), then either
case t has no successors and t trivially, or
In this case, we also have either t 2 \Phi(' 1 ) or for every u such
that R(t; u), u 2 \Phi(').
. be a fair path from s. Note that no s i can
satisfy the first condition above. If s i is such that for all
the induction hypothesis implies that s
then the induction hypothesis implies for all j - i, s j
the path satisfies hence we have s
Now let
Lemma 6 Define a relation H ' S 0 \Theta S by
then for every subformula or elementary formula ' of /, s 0
Proof The proof proceeds by induction on the structure of ', where the base cases for the
induction are the elementary subformulas of /, plus true and false.
1. If so the result is trivial. If
then by the definition of H , s 0
2. If negated atomic proposition, then s 0
3. If
By the induction hypothesis, s 2
case when
4. If
Given
there are three cases.
(a) If no fair paths start at s 0 , then s 0 . The induction hypothesis implies
(b) If s 0 then by the induction hypothesis, s 2 \Phi(' 2 ), and so s 2 \Phi(').
(c) Otherwise, s 0 By the induction hypothesis, s 2
In all cases, s 2 \Phi(8(' 1 U ' 2 )).
5. If
(a) no fair paths start at s 0 , in which case s 0 false and the induction hypothesis
implies s 2 \Phi('), or
so by the induction hypothesis, s 2 \Phi(' 2 ). Also, either s 0
or s 0 Applying the induction hypothesis again, either s 2
In both cases, s 2 \Phi(').
Thus in all cases, s 2
Lemma 7 The relation H given above is a homomorphism.
Proof Note that for every state s 0 of M 0 , there is a (single) state s of M such that H(s 0 ; s).
Let A be the set of atomic propositions for M , and assume H(s 0 ; s). We have
g. From the definition of H,
2 . is a fair path from s 0 . Let 8X' 1 , 8X' 2 ,
. , 8X' n be all the formulas of the form 8X' in el(/) which s 0 satisfies. Then we have
be the state of M related to s 0
1 by H. By the
previous Now by the definition of H, the
formulas of the form 8X' in s must be exactly 8X' 1 , 8X' 2 , . , 8X' n . Then from the
definition of R, we see that R(s; s 1 ). Since H(s 0
continue the process. Defining
we get a sequence of states . starting at s such that H(s 0
To complete the proof, we must show that this sequence is fair.
Assume that - is not fair. Looking at F, we see that there must be some elementary
subformula 8X8(' a U' b ) such that inf(-) " \Phi(8X 8(' a U' b
Consider one of the states s i . s then the
definition of H implies s 0
In addition, the previous lemma implies that if
so that for all j - i,
. is a fair path in M 0 starting at s 0
, and every state on this path
satisfies :' b . But s 0
Hence - is in fact a fair path in M .Theorem 5 M 0
Proof Suppose M 0 - T(/). By lemma 5 and the definition of the tableau, every initial
state of T(/) satisfies /, i.e., T(/)
then by definition, every s 0
By the definition of H, every
such
0 is paired with a (unique) s 0 . Lemma 6 implies that s 0 2 \Phi(/), and by the definition
of the tableau, s 0 2 S 0 . By lemma 7, H is a homomorphism, so M 0 - T(/). 2
The tableau construction can also be used to reason about formulas. We are typically
interested in whether every model of a formula ' is also a model of some other formula /.
relation.
Proposition
Proof If ' then every model of ', in particular T('), is also a model of /. Assume
By the previous corollary, M - T('). Since T(')
We will sometimes extend the set of elementary formulas of a formula by adding additional
atomic propositions. For example, if we wished to check whether true implied p, we
would extend the set of atomic propositions for true to include p (another way to view this
is to imagine rewriting true as true - (p - :p). The formula / has a nontrivial model iff it
is not the case that / j= 8X false. / is true in every model iff true
7 Checking for homomorphism
In this section, we discuss the problem of determining whether there exists a homomorphism
between two structures M and M 0 . Our goal is to efficiently determine if M - M 0 . First note
that if H 1 and H 2 are homomorphisms, then H 1 [H 2 is a homomorphism. Also, ; is trivially
a homomorphism. These facts imply that there is a maximal homomorphism under set
inclusion. We will actually give an algorithm for computing this maximal homomorphism.
We also note the following facts.
1. If s is a state of M and no fair paths start at s, then s is homomorphic to exactly
those states s 0 in M 0 for which
2. If s 0 is a state of M 0 and no fair paths start at s 0 , then s 0 is homomorphic exactly to
those states s in M which are the start of no fair path and for which L(s)"A
States which are the start of no fair path can be detected in polynomial time [12] and
eliminated in a preprocessing step. Hence, without loss of generality, we can assume that
every state in M and M 0 is the start of some fair path. We now describe polynomial time
algorithms for checking the preorder in several important special cases.
Suppose that M 0 has a trivial acceptance condition, i.e., F
Definition 19 Define a sequence of relations H i as follows.
1.
2. H
to be the first H i such that H (such an i exists since H j+1 ' H j for all
j and each H j is finite).
Theorem 6 For every s 2 S and s 0
Proof We first note that H ! is the greatest fixed point of the equation
Suppose s and s 0 are states such that H ! (s; s 0 ). We have
. is a fair path starting from s. From the
above equation, there exists a state s 0
1 such that R 0
Continuing in this
fashion, we find a path s 0
. starting from s 0 such that H ! (s
this path is fair. Hence H ! is a homomorphism from s to s 0 , i.e., s - s 0 .
To show that s - s 0 implies H ! (s; s 0 ), we show that any homomorphism H is a fixed
point of the above equation. Since H ! is the greatest fixed point, we will have H
Hence if there is some homomorphism H such that H(s; s 0 It is enough to
show that H is a subset of the set
If H(s; s 0 ), then we have then by our earlier assumption, there
exists a fair path from t. Hence, letting s t, there is some fair path s 0 s 1 .
from s through t. Since H(s; s 0 ), there exists a fair path s 0
1 . from s
0 such that
1 , we see that (s; s 0 ) is in the above set. 2
We note that H which is at most jSj \Delta jS 0 j. Each H j+1 can also be
computed in polynomial time from H can be computed in polynomial time.
Another important case is when M 0 is deterministic, i.e., if R 0
the language of s is contained in the language of s 0
(the language for a state s is the set of sequences of labelings which occur along the fair
paths starting at s). This relation can be checked in polynomial time using the techniques
of Clarke, Draghicescu and Kurshan [2].
Finally, if M 0 is the result of a tableau construction, say M then as shown in
the previous section, checking whether M - M 0 reduces to the problem of checking whether
8 An example
We have implemented a BDD-based model checker based on the theory developed in the previous
sections. The model checker is written in a combination of T (Yale's dialect of Scheme)
and C. It includes facilities for model checking, temporal reasoning (via the tableau construc-
tion), and checking for homomorphism. To illustrate the system, we use the controller of a
simple CPU as an example. The controller is written in a state machine description language
called CSML [5] which is compiled into Moore machines. We give only a brief description of
the CPU here; Clarke, Long and McMillan [5] give details. The CPU is a simple stack-based
machine, i.e., part of the CPU's memory contains a stack from which instruction operands
are popped and onto which results are pushed. There are two parts to the CPU controller.
The first part is called the access unit and is responsible for all the CPU's memory refer-
ences. The second part, called the execution unit, interprets the instructions and controls
the arithmetic unit, shifter, etc. These two parts operate in parallel. The access unit and
execution unit communicate via a small number of signals. Three of the signals, push, pop
and fetch , are inputs of the access unit and indicate that the execution unit wants to push or
pop something from the stack or to get the next instruction. For each of these signals there
is a corresponding ready output from the access unit. The execution unit must wait for the
appropriate ready signal before proceeding. One additional signal, branch, is asserted by
the execution unit when it wants to jump to a new program location.
In order to increase performance, the access unit attempts to keep the value on the top
of the stack in a special register called the TS register. The goal is to keep the execution
unit from having to wait for the memory. For example, when the TS register contains valid
data, a pop operation can proceed immediately. In addition, when a value is pushed on the
stack, it is moved into this register and copied to memory at some later point. The access
unit also loads instructions into a queue when possible so that fetches do not require waiting
for the memory. This queue is flushed whenever the CPU branches.
Clarke, Long and McMillan gave a number of correctness conditions for the controller.
We demonstrate here how these formulas can be verified in a compositional fashion. From
the form of the conditions, we divide them into three classes. The first class consists of
simple safety properties of the access unit. For example, one of these formulas is
which states that if the access unit outputs the top-of-stack pointer as a memory address,
then it is either reading or writing the TS register. The model checker verified that each of
these properties held for the access unit alone. Hence, they hold in any system containing
the access unit.
The conditions in the second class are slightly more complex. These properties are
safety properties which specify what sequences of operations are allowed. For example, one
condition is
pushed ! 8X8(tsstored - popped V :(pushed - tsload))
Here pushed is an abbreviation for push - pushrdy, and popped abbreviates pop - poprdy.
The formula asserts that if a push operation is completed, then another push cannot be
completed and the access unit cannot attempt to load the TS register from memory until
either a pop occurs or the TS register is stored on the stack. In other words, once the
register contains a value which needs to be pushed on the stack, the CPU cannot do
anything that would destroy this value until the value is either used or successfully stored
in memory. Since all of the properties in this class essentially specify when the access unit
may assert its ready signals, it is tempting to check whether they hold for the access unit
alone as well. This is not possible, however, because the properties also depend on how
the memory acknowledgment signal behaves. To verify these properties, we made a simple
model of the memory (see figure 1). For conciseness, the figure shows a Moore machine;
the actual model used is obtained by adding the fairness constraint shown in the figure
to the structure corresponding to this Moore machine. All of the properties in this class
except for one turn out to be true in the system composed of the access unit and this model
of the memory. The exception is an analog to the previous formula that deals with what
occurs after a pop. The counterexample produced by the model checker for this formula
showed that the formula was false because a push and a pop could occur simultaneously.
When we examined the access unit, we saw that it had been designed assuming that these
operations would be mutually exclusive. The formula turns out to be true with the additional
assumption 8G(:push - :pop). The model checker verified this by building the tableau for
this assumption, composing it with the access unit and memory model, and checking the
formula.
F is defined by
memrd - memwr
memack

Figure

1: Memory abstraction
The final class of criteria consists of a single liveness property: 8G8F(fetch - fetchrdy).
This formula states that the CPU always fetches another instruction. We demonstrate two
different ways of verifying this property.
One way is to observe that for this formula to be true, it must obviously be the case that
the memory responds to requests eventually and that the execution unit does not execute
infinite sequences of pushes, pops and branches. The memory model already has a fairness
constraint ensuring the first of these, but there is nothing to guarantee the second. We can
take care of this by using a simple model of the execution unit (see figure 2). Again, the
actual model is the structure derived from the Moore machine, plus the indicated fairness
constraint. The output idle in this figure is an abbreviation for :(push-pop-fetch-branch).
The model checker verified that the access unit plus the models of the execution unit and
the memory satisfied the above formula. It also verified that there was a homomorphism
between the (structure for the) actual execution unit and the model. Thus, we can conclude
that this formula holds in the final system provided there is a homomorphism from the
actual memory to our model. We also checked that the execution unit model satisfied
the assumption 8G(:push - :pop) used above. Since there is a homomorphism from the
execution unit to the model, we know that the execution unit must satisfy this assumption as
well. This final step allows us to conclude that the composition of the access and execution
units satisfies the entire specification provided the memory is homomorphic to the model we
used.
:fetchrdy
:pushrdy
:poprdy
fetchrdy
pushrdy
poprdy
F is defined by
branch
fetch
idle
push
pop

Figure

2: Execution unit abstraction
We can also verify the final property using a series of 8CTL assumptions. The idea will
be to check the property for the execution unit. In order for the formula to be true, the
access unit must eventually respond to push and pop requests and must fill the instruction
queue when appropriate. We can only guarantee that the access unit meets these conditions
if we know that the execution unit does not try to do two operations at once and that it
will not remove a request before the corresponding operation can complete. We begin with
these properties.
:(fetch
(1)
(2)
The first of these specifies that every pair of operations the execution unit can perform are
mutually exclusive. The other two formulas state that if the execution unit makes a push
or pop request, then it does not deassert the request until the operation completes. The
model checker verified that these properties hold in the execution unit alone, and (using the
tableau construction) that the first property implies the assumption 8G(:push -:pop) used
above. Now using formulas 1 and 2 as assumptions, we checked that the system composed
of the access unit and the memory model satisfied the formula
This specification states that every push operation will be completed. Similarly, using formulas
1 and 3 as assumptions, we verified
The system composed of the access unit and the memory model also satisfies the formula
8G8F(fetchrdy - branch) (at any point, either the access unit will eventually fill
the instruction queue or a branch will occur). Finally, using this formula and formulas
4 and 5 as assumptions, the model checker verified that the execution unit satisfies
8G8F(fetch - fetchrdy). (Again, to complete the verification we would have to demonstrate
a homomorphism between the actual memory and our model of it.)
9 Conclusion
We have identified a subset, 8CTL*, of CTL* which is appropriate for compositional rea-
soning. For this subset, satisfaction is preserved under composition; hence a standard model
checking algorithm can be used to answer the question: Is a formula true for all systems
containing a specified component? We have also proposed a preorder - which is appropriate
for 8CTL*. The preorder captures the relation between a component and a system containing
that component. It provides the basis for using an assume-guarantee style of reasoning
with the logic. Assumptions which are given as structures are discharged by checking the
preorder. We have given a tableau construction for the 8CTL subset of 8CTL*. Satisfaction
of a 8CTL formula corresponds to being below the tableau of the formula in the preorder.
The construction makes it possible to use 8CTL formulas as assumptions and to do temporal
reasoning. 8CTL also has an efficient model checking algorithm. We have implemented a
verification system based on these results and have used it to verify some nontrivial
systems in a compositional fashion.
There are several directions for future work. Intuitively, the 8CTL* subset of CTL*
should be maximal in the sense that any formula for which satisfaction is preserved under
composition should be equivalent to a formula of 8CTL*, but we have not proved this.
Another idea is to look at different logics with the same flavor, such as 8CTL* extended with
automata operators or the -calculus with only [\Delta] modalities. It would also be interesting to
try to extend the tableau construction of section 6 to all of 8CTL*. In order to accomplish
this however, it will almost certainly be necessary to use a more complex type of structure
than that given in definition 2. Another question is whether it is possible to apply our ideas
to branching-time logics with existential path quantifiers. For example, is there a reasonable
algorithm which will determine whether a CTL formula is true in all systems containing
a given component? It is fairly easy to come up with algorithms which are sound, but
completeness seems more difficult to achieve. We also wish to examine the problem of
efficiently checking the preorder for arbitrary structures. Finally, it is essential to try to
apply the compositional reasoning methods we have considered to more complex systems in
order to evaluate the techniques.



--R

Symbolic model checking: 10 20 states and beyond.
A unified approach for showing language containment and equivalence between various types of
Automatic verification of finite-state concurrent systems using temporal logic specifications
Compositional model checking.
A language for compositional specification and verification of finite state hardware controllers.

"partial"
Verifying temporal properties of sequential machines without building their state diagrams.

Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits
"Sometimes"
Efficient model checking in fragments of the propositional mu-calculus
Compositional minimization of finite state processes.
Introduction to Automata Theory
Verifying the correctness of AADL-modules using model checking
Analysis of discrete event coordination.

A structural induction theorem for processes.
The expressive power of implicit specifications.
Checking that finite state concurrent programs satisfy their linear specification.

A Calculus of Communicating Systems
In transition for global to modular temporal reasoning about programs.
Network grammars
The modular framework of computer-aided verification: Moti- vation
Local model checking in the modal mu-calculus
Bisimulations and divergence.
Compositional checking of validity on finite state processes.
Model checking in the modal
--TR
MYAMPERSANDldquo;SometimesMYAMPERSANDrdquo; and MYAMPERSANDldquo;not neverMYAMPERSANDrdquo; revisited
Automatic verification of finite-state concurrent systems using temporal logic specifications
A structural induction theorem for processes
Trace theory for automatic hierarchical verification of speed-independent circuits
Compositional model checking
The concurrency workbench
Network grammars, communication behaviors and automatic verification
Verifying the correctness of AADL modules using model checking
Analysis of discrete event coordination
A unified approach for showing language containment and equivalence between various types of MYAMPERSANDohgr;-automata
In transition from global to modular temporal reasoning about programs
Tableau-based model checking in the propositional mu-calculus
The expressive power of implicit specifications
A note on model checking the model MYAMPERSANDngr;-calculus
Checking that finite state concurrent programs satisfy their linear specification
A Calculus of Communicating Systems
Introduction To Automata Theory, Languages, And Computation
Local Model Checking in the Modal Mu-Calculus
The Modular Framework of Computer-Aided Verification
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams
Compositional Minimization of Finite State Systems
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic

--CTR
Pallab Dasgupta , Arindam Chakrabarti , P. P. Chakrabarti, Open Computation Tree Logic for Formal Verification of Modules, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.735, January 07-11, 2002
Robert John Walters, Checking of models built using a graphically based formal modelling language, Journal of Systems and Software, v.76 n.1, p.55-64, April 2005
Alma L. Juarez Dominguez , Nancy A. Day, Compositional reasoning for port-based distributed systems, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
I. S. W. B. Prasetya , S. D. Swierstra, Factorizing fault tolerance, Theoretical Computer Science, v.290 n.2, p.1201-1222, 2 January
David Harel , Orna Kupferman , Moshe Y. Vardi, On the complexity of verifying concurrent transition systems, Information and Computation, v.173 n.2, p.143-161, March 15, 2002
Yunshan Zhu , James H. Kukula, Generator-based Verification, Proceedings of the IEEE/ACM international conference on Computer-aided design, p.146, November 09-13,
K. Mani Chandy , Michel Charpentier, An Experiment in Program Composition and Proof, Formal Methods in System Design, v.20 n.1, p.7-21, January 2002
Arindam Chakrabarti , Pallab Dasgupta , P. P. Chakrabarti , Ansuman Banerjee, Formal verification of module interfaces against real time specifications, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
R. S. Lazi , T. C. Newcomb , A. W. Roscoe, On model checking data-independent systems with arrays without reset, Theory and Practice of Logic Programming, v.4 n.5-6, p.659-693, September 2004
Doron Bustan , Orna Grumberg, Simulation-based minimization, ACM Transactions on Computational Logic (TOCL), v.4 n.2, p.181-206, April
Jason Baumgartner , Tamir Heyman , Vigyan Singhal , Adnan Aziz, An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists, Formal Methods in System Design, v.23 n.1, p.39-65, July
Juergen Dingel, Computer-assisted assume/guarantee reasoning with VeriSoft, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Yonit Kesten , Nir Piterman , Amir Pnueli, Bridging the gap between fair simulation and trace inclusion, Information and Computation, v.200 n.1, p.35-61, 1 July 2005
Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.390-402, January 19-21, 2000, Boston, MA, USA
Thomas A. Henzinger , Orna Kupferman , Sriram K. Rajamani, Fair simulation, Information and Computation, v.173 n.1, p.64-81, February 25, 2002
Ferucio Laurentiu Tiplea , Aurora Tiplea, Petri net reactive modules, Theoretical Computer Science, v.359 n.1, p.77-100, 14 August 2006
M. Clarke , O. Grumberg , S. Jha, Verifying parameterized networks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.726-750, Sept. 1997
Adnan Aziz , Thomas Shiple , Vigyan Singhal , Robert Brayton , Alberto Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking, Formal Methods in System Design, v.21 n.2, p.193-224, September 2002
Peter Henderson, Modelling architectures for dynamic systems, Programming methodology, Springer-Verlag New York, Inc., New York, NY,
Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999
Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.2, p.339-369, March 2004
Orna Kupferman , Moshe Y. Vardi, An automata-theoretic approach to modular model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.87-128, Jan. 2000
Yunja Choi , Sanjai Rayadurgam , Mats P.E. Heimdahl, Automatic abstraction for model checking software systems with interrelated numeric constraints, ACM SIGSOFT Software Engineering Notes, v.26 n.5, Sept. 2001
Doron Bustan , Orna Grumberg, Applicability of fair simulation, Information and Computation, v.194 n.1, p.1-18, 10 October 2004
Xudong He , Huiqun Yu , Tianjun Shi , Junhua Ding , Yi Deng, Formally analyzing software architectural specifications using SAM, Journal of Systems and Software, v.71 n.1-2, p.11-29, April 2004
Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001
Arindam Chakrabarti , Patrice Godefroid, Software partitioning for effective automated unit testing, Proceedings of the 6th ACM & IEEE International conference on Embedded software, October 22-25, 2006, Seoul, Korea
Thomas A. Henzinger , Orna Kupferman , Rupak Majumdar, On the universal and existential fragments of the -calculus, Theoretical Computer Science, v.354 n.2, p.173-186, 28 March 2006
Ansuman Banerjee , Pallab Dasgupta, The open family of temporal logics: Annotating temporal operators with input constraints, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.3, p.492-522, July 2005
F. Zaraket , J. Baumgartner , A. Aziz, Scalable compositional minimization via static analysis, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1060-1067, November 06-10, 2005, San Jose, CA
Mats P. Heimdahl , Devaraj George, On the effect of test-suite reduction on automatically generated model-based tests, Automated Software Engineering, v.14 n.1, p.37-57, March     2007
Sharon Barner , Orna Grumberg, Combining symmetry reduction and under-approximation for symbolic model checking, Formal Methods in System Design, v.27 n.1/2, p.29-66, September 2005
Dongfeng Wang , Farokh B. Bastani , I. -Ling Yen, Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance, IEEE Transactions on Software Engineering, v.31 n.9, p.713-732, September 2005
S. Chouali , J. Julliand , P.-A. Masson , F. Bellegarde, PLTL-partitioned model checking for reactive systems under fairness assumptions, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.267-301, May 2005
Mauro Caporuscio , Paola Inverardi , Patrizio Pelliccione, Compositional Verification of Middleware-Based Software Architecture Descriptions, Proceedings of the 26th International Conference on Software Engineering, p.221-230, May 23-28, 2004
Andrew D. Gordon , Alan Jeffrey, Authenticity by typing for security protocols, Journal of Computer Security, v.11 n.4, p.451-519, 01/01/2004
David Dharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA,
Frdric Herbreteau , Franck Cassez , Olivier Roux, Application of Partial-Order Methods to Reactive Programswith Event Memorization, Real-Time Systems, v.20 n.3, p.287-316, May 2001
Kathi Fisler , Moshe Y. Vardi, Bisimulation Minimization and Symbolic Model Checking, Formal Methods in System Design, v.21 n.1, p.39-78, July 2002
Compositional analysis for verification of parameterized systems, Theoretical Computer Science, v.354 n.2, p.211-229, 28 March 2006
de la Riva , Javier Tuya, Automatic generation of assumptions for modular verification of software specifications, Journal of Systems and Software, v.79 n.9, p.1324-1340, September 2006
R. Gentilini , C. Piazza , A. Policriti, From Bisimulation to Simulation: Coarsest Partition Problems, Journal of Automated Reasoning, v.31 n.1, p.73-103,
Hakan Erdogmus, Architecture-driven verification of concurrent systems, Nordic Journal of Computing, v.4 n.4, p.380-413, Winter 1997
Tevfik Bultan , Richard Gerber , William Pugh, Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.747-789, July 1999
Sara Gradara , Antonella Santone , Maria Luisa Villani, Using heuristic search for finding deadlocks in concurrent systems, Information and Computation, v.202 n.2, p.191-226, 1 November, 2005
Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
temporal logics;formal verification;computer-aided verification;CTL;moore machines;model checking