Sciweavers

Share
TACAS
1998
Springer

Verification of Large State/Event Systems Using Compositionality and Dependency Analysis

9 years 10 months ago
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.
Jørn Lind-Nielsen, Henrik Reif Andersen, Ge
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1998
Where TACAS
Authors Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre J. Kristoffersen, Kim Guldstrand Larsen
Comments (0)
books