Verification of Large State/Event Systems Using Compositionality and Dependency Analysis.
A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to significantly improve the efficiency of symbolic model checking of state/event models. It makes possible automated verification of large industrial designs with the use of only modest resources (less than 5 minutes on a standard PC for a model with 1421 concurrent machines). The results of the paper are being implemented in the next version of the commercial tool visualSTATETM.
Introduction
Symbolic model checking is a powerful technique for formal verification of finite-state
concurrent systems. The technique was initially developed to verify digital
systems and for this class of systems, it has proven very efficient: hardware
systems with an extremely large number of reachable states has been verified.
However, it is not clear whether model checking is effective for other kinds of
concurrent systems as, for example, software systems. One reason that symbolic
model checking may not be as efficient is that software systems tend to be
both larger and less regularly structured than hardware. For example, many
of the results reported for verifying large hardware systems have been for linear
structures like stacks or pipelines (see, e.g., [7]) for which it is known [17] that the
size of the transition relation (when represented as an ROBDD) grows linearly
with the size of the system. Only recently has the first experiments on larger
realistic software systems been reported [3, 18].
? Supported by CIT, The Danish National Center of IT Research
?? BRICS (Basic Research in Computer Science) is a basic research center funded by
the Danish government at Aarhus and Aalborg
This paper presents a new technique that significantly improves the performance
of symbolic model checking on embedded reactive systems modeled using
a state/event model. The state/event model is a concurrent version of Mealy ma-
chines, that is, it consists of a fixed number of concurrent finite state machines
that have pairs of input events and output actions associated with the transitions
of the machines. The model is synchronous: each input event is reacted
upon by all machines in lock-step; the total output is the multi-set union of the
output actions of the individual machines. Further synchronization between the
machines is achieved by associating a guard with the transitions. Guards are
Boolean combinations of conditions on the local states of the other machines.
In this way, the firing of transitions in one machine can be made conditional on
the local state of other machines. If a machine has no enabled transition for a
particular input event, it simply does not perform any state change.
The state/event model is convenient for describing the control portion of
embedded reactive systems, including smaller systems as cellular phones, hi-fi
equipment, and cruise controls for cars, and large systems as train simulators,
flight control systems, telephone and communication protocols. The model is
used in the commercial tool visualSTATE tm [16]. This tool assists in developing
embedded reactive software by allowing the designer to construct a state/event
model and analyze it by either simulating it or by running a consistency checker.
The tool automatically generates the code for the hardware of the embedded
system. The consistency checker is in fact a verification tool that checks for a
range of properties that any state/event model should have. Some of the checks
must be passed for the generated code to be correct, for instance, it is crucial
that the model is deterministic. Other checks are issued as warnings that might
be design errors such as transitions that can never fire.
State/event models can be extremely large. And unlike in traditional model
checking, the number of checks is at least linear in the size of the model. This paper
reports results for models with up to 1421 concurrent state machines (10 476
states). For systems of this size, traditional symbolic model checking techniques
fail, even when using a partitioned transition relation [5] and backwards itera-
tion. We present a compositional technique that initially considers only a few
machines in determining satisfaction of the verification task and, if necessary,
gradually increases the number of considered machines. The machines considered
are determined using a dependency analysis of the structure of the system.
The results are encouraging. A number of large state/event models from
industrial applications have been verified. Even the largest model with 1421
concurrent machines can be verified with modest resources (it takes less than an
hour on a standard PC). Compared with the current version of visualSTATE tm ,
the results improve on the efficiency of checking the smaller instances and dramatically
increase the size of systems that can be verified.
Related Work
The use of ROBDDs [4] in model checking was introduced by Burch et al. [6]
and Coudert et al. [12]. Several improvements have been developed since, such
as using a partitioned transition relation [5, 13] and simplifying the ROBDD
representation during the fixed-point iteration [11]. Many of these improvements
are implemented in the tool SMV [17]. Other techniques like abstraction [9]
and compositional model checking [10] further reduce the complexity of the
verification task, but require human insight and interaction.
The experiments by Anderson et al. [3] and Sreemani and Atlee [18] verified
large software systems using SMV. The technique presented here significantly
improves on the results we have obtained using SMV and makes it possible
to verify larger systems. The compositional technique shares ideas with partial
model checking [1, 2, 15], but explicitly analyzes the structure of the model.
Outline
The state/event model is described in section 2. Section 3 explains how the range
of consistency checks performed by visualSTATE tm are reduced to two simple
types of checks. Section 4 shows how state/event systems are encoded by ROB-
DDs. The compositional technique and the dependency analysis is introduced
in section 5, and further developed in section 6. The technique is evaluated in
section 7 and section 8 draws some conclusions.
State/Event Systems
A state/event system consists of n machines over an input (or event)
alphabet E and an output alphabet O. Each machine M i is a triple (S
of local states, an initial state, and a set of transitions. The set of transitions is
a relation
where M(O) is a multi-set of outputs, and G i is the set of guards not containing
references to machine i. These guards are generated from the following simple
grammar for Boolean expressions:
The atomic predicate l is read as "machine j is at local state p" and
tt denotes a true guard. The global state set of the state/event system is the
product of the local state sets: S The guards are interpreted
straightforwardly over S: for any s 2 S, s exactly when the
j'th component of s is p. The notation g[s j =l j ] denotes that s j is
substituted for l j , with occurrences of atomic propositions of the form l
replaced by tt or :tt depending on whether s j is identical to p.
Considering a global state s, all guards in the transition relation can be
evaluated. We define a version of the transition relation in which the guards
have been evaluated. This relation is denoted s e
expressing that machine
when receiving event e makes a transition from s i to s 0
i and generates output
o. Formally,
e
e
e
Fig. 1. Two state/event machines and the corresponding parallel combination. The
guards, which formally should be of the form l are simply written as the state p
since the location l j is derivable from the name of the state. The small arrows indicate
the initial states. The reference to r is a requirement to a state in a third machine not
shown.
Two machines can be combined into one. More generally if M I and M J
are compositions of two disjoint sets of machines I and J , I ; J '
we can combine them into one M
I \Theta S J ands 0
J ). The transition relation T IJ is a subset of
S IJ \Theta E \Theta G IJ \Theta M(O) \Theta S IJ , where G IJ are the guards in the composite
machine. By construction of T IJ , the guards G IJ will not contain any references
to machines in I [ J . To define T IJ , we introduce the predicate idle:
I
which holds for states in which no transitions in M I are enabled at state s I
when receiving event e. The transition relation T IJ is defined by the following
inference rules (the symbol ] denotes multi-set union):
I
I
In particular, the full combination of all n machines yields a Mealy machine in
which the transitions s e
\Gamma\Gamma! s 0 are defined by
Y
is true:
The state/event systems in figure 1 illustrates two machines and the parallel
composition of them. By synchronizing on the same event e they are restricted
to a cyclic iteration through the total state space with the side effect that they
will generate the output when they are finished.
3 Consistency Checks
The consistency checker in visualSTATE tm performs seven predefined types of
checks, each of which can be reduced to verifying one of two types of properties.
The first type is a reachability property. For instance, visualSTATE tm performs a
check for "conflicting transitions", i.e., it checks whether two or more transitions
can become enabled in the same local state, leading to non-determinism. This
can be reduced to questions of reachability by considering all pairs of guards g 1
and g 2 of transitions with the same local state s i and input event e. A conflict
can occur if a global state is reachable in which (l
In total, five of the seven types of checks reduce to reachability checks. Four
of these, such as check for transitions that are never enabled and check for
states that are never reached, generate a number of reachability checks which is
linear in the number of transitions, t. In the worst-case the check for conflicting
transitions gives rise to a number of reachability checks which is quadratic in
the number of transitions. However, in practice very few transitions have the
same starting local state and input event, thus in practice the number of checks
generated is much smaller than t.
The remaining two types of consistency checks reduce to a check for absence
of local deadlocks. A local deadlock occurs if the system can reach a state in
which one of the machines idles forever on all input events. This check is made
for each of the n machines. In total at least t checks have to be performed
making the verification of state/event systems quite different from traditional
model checking where typically only a few key properties are verified.
We attempt to reduce the number of reachability checks by performing a
implicational analysis between the guards of the checks. If a guard g 1 implies
another guard g 2 then clearly, if g 1 is reachable so is g 2 . To use this information
we start by sorting all the guards in ascending order of the size of their satisfying
state space. In this way the most specific guards are checked first and for each
new guard to be checked we compare it to all the already checked (and reachable)
guards. If the new guard includes one of them, then we know that it is satisfiable.
In the worst-case this is a quadratic number of tests. However, in our experiments
a reduction between 40% and 94% is obtained.
4 ROBDD Representation
This section describes how Reduced Ordered Binary Decision Diagrams (ROB-
DDs) [4] are used to represent sets of states and the transition relation. We also
show how to perform a forward iteration to construct the set of reachable states
from which it is straightforward to check each of the reachability checks.
To construct the ROBDD e
T for the transition relation T , we first construct
the local transition relations e
for each machine M i . The variables of
the ROBDD represents an encoding of the inputs, the current states and the
next-states. The variables are ordered as follows: The first kEk variables encodes
the input events E (kXk denotes dlog 2 jXje) and are denoted VE . Then
encoding the current- (un-
primed variables) and the next-states (primed variables) for machine i.
The transition relation e
constructed as an ROBDD predicate
over these variables. We construct the ROBDD for a transition (s
by the conjunction of the ROBDD encoding s i , e, g, and s 0
. (The outputs are
not encoded as they have no influence on the reachable states of the system.)
The encoding of s i , e, and s 0
i is straightforward and the encoding of the guard
g is done by converting all atomic predicates l to ROBDD predicates over
the current-state variables for machine M j and then performing the Boolean
operations in the guard. The encoding of all transitions of machine i is obtained
from the disjunction of the encoding of the individual transitions:
where e
e is the ROBDD encoding of input e and e s i and e s 0
i are the ROBDD
encodings of the current-state s i and next-state s 0
To properly encode the global transition relation T , we need to deal with
situations where no transitions of T i are enabled. In those cases we want the
machine i to stay in its current state. We construct an ROBDD neg i representing
that no transition is enabled by negating all guards in machine i (including the
The ROBDD equ i encodes that machine i does not change state by requiring
that the next-state is identical to the current-state:
The local transition relation for machine i is then:
e
The ROBDD e
T for the full transition relation is the conjunction of the local
transition relations:
e
e
One way to check whether a state s is reachable is to construct the reachable
state space R. The construction of R can be done by a standard forward iteration
of the transition relation, starting with the initial state s 0 :
where V is the set of current-state variables, V 0 is the set of next-state variables,
and denotes the result of replacing all the primed variables in V 0 by
their unprimed versions.
The construction of the full transition relation T can be avoided by using
a partitioned transition relation [5]. The local transition relations T i are used
without ever building the full
Both approaches have been implemented and tested on our examples as shown in
section 7. Here we see that the calculation of the reachable state space using the
full transition relation is both fast and efficient for the small examples. However,
for models with more than approximately machines, both approaches fail to
complete.
Compositional Backwards Reachability
The problems of forwards iteration can typically be solved by using a backwards
reachability analysis. The verification task is to determine whether a guard g can
be satisfied. Instead of computing the reachable state space and check that g is
valid somewhere in this set, we start with the set of states in which g is valid and
compute in several backwards iterations, states that can reach a state in which
g is satisfied. The goal is to determine whether the initial state is among these
states. Our novel idea is to perform the backwards iteration in a compositional
manner considering only a minimal number of machines. Initially, only machines
mentioned in g will be taken into account. Later also machines on which these
depend will be included.
Notice that compared to the forwards iteration, this approach has an apparent
drawback when performing a large number of reachability checks: instead
of just one fixed-point iteration to construct the reachable state space R (and
then trivially verify the properties), a new fixed-point iteration is necessary for
each property that is checked. However, our experiments clearly demonstrate
that when using a compositional backwards iteration, each of the fixed-point
iterations can be completed even for very large models whereas the forwards
iteration fails to complete the construction of R for even medium sized models.
To formalize the backwards compositional technique, we need a semantic version
of the concept of dependency. For a subset of the machines I '
two states s; s 0 2 S are I-equivalent, written
. If
a subset P of the reachable states S only is constrained by components in some
index set I we can think of P as having I as a sort. This leads to the following
definition: A subset P of S is I-sorted if for all s; s
s I
M3
Fig. 2. The left figure is an example showing the effect of BI (g). If X is the guard
Y the guard l I then the transitions from sI seem to
depend on machines M j and Mk outside I. However, the guards X, :X Y , and :Y
together span all possibilities and therefore by selecting either e1 , e2 , or e3 the state
sI can reach g irrespective of the states of the machines M j and Mk . The right figure
illustrates the dependencies between 9 state machines taken from a real example (the
example "hi-fi" of section 7). An arrow from one machine M i to another M j indicates
the existence of a transition in M i with a guard that depends on a state in machine
As an example, consider a guard g which mentions only machines 1 and 3. The
set of states defined by g is I-sorted for any I containing 1 and 3. 1 Another
understanding of the definition is that a set P is I-sorted if it is independent of
the machines in the complement I ng n I .
From an I-sorted set g we will perform a backwards reachability computation
by including states which, irrespective of the states of the machines in I , can
reach g. One backward step is given by the function B I (g) defined by:
\Gamma\Gamma! s 00 and s 00
(1)
By definition B I (g) is I-sorted. The set B I (g) defined by B I is the set of states
which independently of machines in I , by some input e, can reach a state in g.
Observe that B I (g) is monotonic in both g and I . Figure 2 shows how a state
s I of a machine is included in B I (g) although it syntactically seems to depend
on machines outside I .
By iterating the application of B I , we can compute the minimum set of states
containing g and closed under application of B I . This is the minimum fixed-point
I (X), which we refer to as B
I (g). Note that B
f1;::: ;ng (g) becomes the
desired set of states which may reach g.
A set of indices I is said to be dependency closed if none of the machines in
I depend on machines outside I . Formally, I is dependency closed if for all i 2 I ,
states inputs e, and outputs o, s e
The basic properties of the sets B
I (g) are captured by the following lemma:
1 If the guard is self-contradictory (always false), it will be I-sorted for any I. This reflects
the fact that the semantic sortedness is more precise than syntactic occurrence.
(Compositional Reachability Lemma). Assume g is an I-sorted
subset of S. For all subsets of machines I, J with I ' J the following holds:
I
2: B
I (g))
3: I dependency closed
I
The results of the lemma are applied in the following manner. To check whether
a guard g is reachable, we first consider the set of machines I 1 syntactically
mentioned in g. Clearly, g is I 1 -sorted. We then compute B
I1 (g). If the initial
state s 0 belongs to B
I1 (g), then by (1) s
f1;::: ;ng (g) and therefore g is
reachable from s 0 and we are done. If not, we extend I 1 to a larger set of
machines I 2 by adding machines that are syntactically mentioned on guards in
transitions of machines in I 1 . We then compute B
I2 (g) as B
I1 (g)) which
is correct by (2). We continue like this until s 0 has been found in one of the
sets or an index set I k is dependency closed. In the latter case we have by (3)
I k
f1;::: ;ng (g) and g is unreachable unless s
I k
(g).
As an example, assume that we want to determine whether the guard
reachable in the example of figure 2 (right). The initial index
set is I 3g. If this is not enough to show g reachable, the second index set
I used. Since this set is dependency closed, g is reachable if and
only if the initial state belongs to B
I1 (g)).
The above construction is based on a backwards iteration. A dual version of
I for a forwards iteration could be defined. However, such a definition would
not make use of the dependency information since s 0 is only I-sorted for I =
ng. Therefore all machines would be considered in the first fixed-point
iteration reducing it to the complete forwards iteration mentioned in the previous
section.
Seemingly, the definition of B I (g) requires knowledge of the global transition
relation, and therefore does not seem to yield any computational advantage.
However, as explained below, using ROBDDs this may be avoided leading to an
efficient computation of B I (g). The ROBDD e
I (eg) representing one iteration
backwards from the states represented by the ROBDD e g can be constructed
immediately from the definition (1):
e
is equal to eg with all variables in V replaced by their primed
versions in V 0 . It is essential to avoid building the global transition relation e
T .
This is done by writing 9V 0 as 9V 0
I :9V 0
I
and e
I where e
i2I
e
This allows us to push the existential quantification of V 0
I
to e
I since g is I-sorted
and thus independent of the variables in V 0
I . As 9V 0
I is a tautology, equation
(2) reduces to:
e
which only uses the local transition relations for machines in I . Each T i refers
only to primed variables in V 0
allowing early variable quantification for each
machine individually:
e
This equation efficiently computes one step in the fixed-point iteration constructing
e
I (eg).
Notice, that the existential quantifications can be performed in any order.
We have chosen the order in which the machines occur in the input, but other
orders might exist which improves performance.
6 Local Deadlock Detection
In checking for local deadlocks we use a construction similar to backwards reach-
ability. To make the compositional backwards lemma applicable we work with
the notion of a machine being live which is the exact dual of having a local
deadlock. In words, a machine is live if it always is the case that there exists a
way to make the machine move to a new local state. Formally, a global state s
is live for machine i if there exists a sequence of states s
and s j e
\Gamma\Gamma! s j+1 (for some e and o) such that s k
i . Machine i is live if all
reachable states are live. A simple example of a state/event system with a local
deadlock is shown in figure 3.
Fig. 3. A state/event system with a local deadlock. The global state
live for the machine to the right since for all input events the guard p1 remains false.
The state s is reachable (e.g., by initially receiving e1) and thus the machine to the
right has a local deadlock.
The check is divided into two parts. First, the set of all live states L
machine i is computed. Second, we check that all reachable states are in L
A straightforward but inefficient approach would be to compute the two sets
and check for inclusion. However, we will take advantage of the compositional
construction used in the backwards reachability in both parts of the check.
Similar to the definition of B I (g), we define L I;i (X) to be the set of states that
are immediately live for machine i 2 I independently of the machines outside I
or leads to states in X (which are states assumed to be live for machine i):
Notice, that compared to definition (1) the only difference is the extra possibility
that the state is immediately live, i.e., s i 6= s 00
. The set of states that are live
for machine i independently of machines outside I is then the set L
I;i (;) where
is the minimum fixed point defined by L
The three properties of lemma 1 also holds for L
If I is dependency closed it follows from property (3) of the lemma that L
equals L
(;) which is precisely the set of live states of machine i. This
gives an efficient way to compute the sets L
I;i (;) for different choices of I .
We start with I 1 equal to fig and continue with larger I k 's exactly as for the
backwards reachability. The only difference is the termination conditions. One
possible termination case is if L
I k ;i (;) becomes equal to S for some k. In that
case it is trivial that the set of reachable states is contained in L
I k ;i (;). From
the monotonicity property (1) of the lemma it follows that machine i is live
and thus free of local deadlocks. The other termination case is when I k becomes
dependency closed. Then we have to check whether there exists reachable states
not in L
I k ;i (;). This is done by a compositional backwards reachability check
with
I k ;i (;).
7 Experimental Results
The technique presented above has been used on a range of real industrial
state/event systems and a set of systems constructed by students in a course on
embedded systems. The examples are all constructed using
They cover a large range of different applications and are structurally highly
irregular.
The examples hi-fi, surround, flow, motor, intervm, dkvm, multicd,
ice1 and ice2 are all industrial examples. hi-fi is the control part of an advanced
compact hi-fi system, surround is a surround sound control unit for a video
player, flow is the control part of a flow meter, motor is a motor control,
intervm and dkvm are advanced vending machines, multicd is the control of a
multi-volume CD player, and ice1 and ice2 are both independent subsystems of
a train simulator. The remaining examples are constructed by students. The vcr
is a simulation of a video recorder, cyber is an alarm clock, jvc is the control
of a compact hi-fi system, video is a video player, and volvo is a simulation of
the complete functionality of the dashboard of a car. The characteristics of the
state/event systems are shown in table 1.
The experiments were carried out on a 166 MHz Pentium PC with
RAM running Linux. To implement the ROBDD operations, we have constructed
our own ROBDD package which is comparable to state-of-the-art packages in
terms of performance. In all experiments we limit the total number of ROBDD
nodes to one million corresponding to 20 MB of memory. We check for each
transition whether the guard is reachable and whether it is conflicting with
other transitions. Furthermore, we check for each machine whether it has a local
deadlock. The total runtime and memory consumption for these checks are shown
in table 2. The total number of checks is far from the quadratic worst-case, which

Table

1. The state/event systems used in the experiments. The last two columns
show the size of the declared and reachable state space. The declared state space is
the product of the number of local states of each machine. The reachable state space
is only reported for those systems where the forwards analysis completes.
System Machines Local states Transitions Declared Reachable
vcr 7
cyber 8 19
dkvm 9
flow
motor 12
surround 12
multicd 28

Table

2. The runtime and memory consumptions of the experiments. The second column
of the table shows the total number of guards that are checked for reachability
after this number has been reduced by the implicational analysis. The forward columns
show results using a forward iteration with a full and a partitioned transition relation.
The backward columns show the results of a backwards iteration using the full transition
relation and the compositional backwards reachability. The visualSTATE column
shows the runtimes obtained using an explicit state enumeration as implemented in version
3.0 of visualSTATE tm . A "\Gamma" denotes that we ran out of memory or the runtime
exceeded two hours without finishing.
Forward Backward
System Guards Full Partitioned Full Compositional visualSTATE
checked Sec MB Sec MB Sec MB Sec MB Sec
cyber
dkvm
flow
motor
surround 173 8.9 6 269.0 14 9.7 6 13.0 6 3780
volvo
multicd 199 4.9
Fig. 4. The fraction of machines actually used in the compositional backwards reachability
analysis of the guards of the largest system ice2. For each size of dependency
closed set, a line between is drawn between the minimum and maximum fraction of
machines used in verifying guards with dependency closed sets of that size. For in-
stance, for the guards with dependency closed sets with 234 machines (the right-most
line) only between 1% and 32% of the machines are needed to prove that the guard is
reachable.
supports the claim that in practice only very few checks are needed to check for
conflicting rules (see section 3).
As expected the forwards iteration with full transition relation is efficient
for smaller systems. It is remarkable that the ROBDD technique is superior to
explicit state enumeration even for systems with a very small number of reachable
states. Using the partitioned transition relation in the forwards iteration
works poorly. This could be due to the fact that we do not use early variable
quantification since this is not as straightforward as for the backwards iteration.
For the two largest systems only the compositional backwards technique suc-
ceeds. In fact, for the four largest systems it is the most efficient and for the
small examples it has performance comparable to the full forward technique.
This is despite the fact that the number of checks is high and the backward iterations
must be repeated for each check. From the experiments it seems that the
compositional backwards technique is better than full forwards from somewhere
around 20 machines.
In order to understand why the compositional backwards technique is successful
we have analyzed the largest system ice2 in more detail, see figure 4.
For each guard we have computed the size of its smallest enclosing dependency
closed set of machines. During the backwards iterations we have kept track of
how many times the set of machines I (used in B
I (g)) need to be enlarged and
how many machines was contained in the set I when the iteration terminated.
The dependency closed sets of cardinality 63, 66, 85, 86, 125, 127 all contain at
least one machine with a guard that is unreachable. As is clearly seen from the
figure, in these cases the iteration has to include the entire dependency closed
set in order to prove that the initial state cannot reach the guard. In fact, only
in the case of unreachable guards is more than 32% of the machines in a dependency
closed set ever needed (ignoring the small dependency closed sets with
less than 12 machines). A reduction of 32% amounts to a reduction in runtime
much larger than a third due to the potential exponential growth of the ROBDD
representation in the number of transition relations e
8 Conclusion
We have presented a verification problem for state/event systems which is characterized
by a large number of reachability checks. A new compositional technique
has been presented which significantly improves on the performance of symbolic
model checking for state/event systems. This has been demonstrated on a variety
of industrial systems several of which could not be verified using traditional
symbolic model checking, e.g., using SMV.
We expect that these results can be translated to other models of embedded
control systems than the state/event model, as for example StateCharts [14].
Furthermore, the two types of checks are of a general nature. Clearly, reachability
is a key property which captures a number of important properties of a system.
Moreover, the check for local deadlock shows how properties requiring nesting of
fixed points can be checked efficiently with the compositional backwards analysis.
Thus, it seems straightforward to implement more general checks as expressed
in, for instance, CTL [8].



--R

Partial model checking with ROBDDs.
Partial model checking (extended abstract).
Model checking large software specifications.

Symbolic model checking with partitioned transition relations.
Symbolic model checking: 10 20 states and beyond.
Symbolic model checking for sequential circuit verification.
Automatic verification of finite-state concurrent systems using temporal logic specifications
Model checking and abstraction.
Compositional model checking.
Verification of synchronous sequential machines based on symbolic execution.
Verifying temporal properties of sequential machines without building their state diagrams.
Efficient model checking by automated ordering of transition relation partitions.
STATECHARTS: A visual formalism for complex systems.
A compositional proof of a read-time mutual exclusion protocol
Beologic r A/S.
Symbolic Model Checking.
Feasibility of model checking software requirements: a case study.
--TR
Graph-based algorithms for Boolean function manipulation
Statecharts: A visual formalism for complex systems
Compositional model checking
Verification of synchronous sequential machines based on symbolic execution
Model checking and abstraction
Requirements Specification for Process-Control Systems
Model checking large software specifications
Tearing based automatic abstraction for CTL model checking
Symbolic Model Checking
Partial Model Checking with ROBDDs
A Compositional Proof of a Real-Time Mutual Exclusion Protocol
Stepwise CTL Model Checking of State/Event Systems
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams
An Iterative Approach to Language Containment
Efficient Model Checking by Automated Ordering of Transition Relation Partitions
Automatic Abstraction Techniques for Propositional MYAMPERSAND#181;-calculus Model Checking
Verification of Hierarchical State/Event Systems Using Reusability and Compositionality
Partial Model Checking
embedded software;symbolic model checking;formal verification;backwards reachability