Verification of Large State/Event Systems using Compositionality
and Dependency Analysis
by Jørn Lind-Nielsen,
Henrik Reif Andersen,
Gerd Behrmann,
Henrik Hulgaard,
Kåre Kristoffersen and
Kim G. Larsen.
In TACAS'98: Tools and Algorithms for the Construction and Analysis of
Systems, Lecture Notes
in Computer Science, Springer.
Abstract
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. This technique makes possible
automated verification of large industrial designs with the use of
only modest resources (less than one hour 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 Visualstate.
[BiBTeX entry]
[Postscript]