Verification of Large State/Event Systems using
                Compositionality and Dependency Analysis.

Jørn Lind-Nielsen; Henrik Reif Andersen; Gerd Behrmann; Henrik Hulgaard; Kaare Kristoffersen; Kim G. Larsen

Verification of Large State/Event Systems using Compositionality and Dependency Analysis.

Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kaare Kristoffersen, Kim G. Larsen

Aalborg University

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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 \emph{compositionality} and \emph{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.

Original language	English
Title of host publication	Proceedings of TACAS'98 (LNCS 1384)
Publisher	Springer Verlag
Publication date	1999
Publication status	Published - 1999
Event	TACAS 98 - Duration: 1 Jan 1997 → …

Conference

Conference	TACAS 98
Period	01/01/1997 → …

OpenUrl availability

Full text

Cite this

@inproceedings{34aa8b65b3ce49b694d19dbdc8b54806,

title = "Verification of Large State/Event Systems using Compositionality and Dependency Analysis.",

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 \emph{compositionality} and \emph{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.",

author = "J{\o}rn Lind-Nielsen and Andersen, {Henrik Reif} and Gerd Behrmann and Henrik Hulgaard and Kaare Kristoffersen and Larsen, {Kim G.}",

year = "1999",

language = "English",

booktitle = "Proceedings of TACAS'98 (LNCS 1384)",

publisher = "Springer Verlag",

address = "Germany",

note = "TACAS 98 ; Conference date: 01-01-1997",

}

TY - GEN

T1 - Verification of Large State/Event Systems using Compositionality and Dependency Analysis.

AU - Lind-Nielsen, Jørn

AU - Andersen, Henrik Reif

AU - Behrmann, Gerd

AU - Hulgaard, Henrik

AU - Kristoffersen, Kaare

AU - Larsen, Kim G.

PY - 1999

Y1 - 1999

N2 - A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses \emph{compositionality} and \emph{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.

AB - A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses \emph{compositionality} and \emph{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.

M3 - Article in proceedings

BT - Proceedings of TACAS'98 (LNCS 1384)

PB - Springer Verlag

T2 - TACAS 98

Y2 - 1 January 1997

ER -