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

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

doi:10.1023/A:1008736219484

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

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

Research output: Contribution to journal › Article › Academic

22 Citations (Scopus)

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. 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 visualSTATE^TM.

Original language	English
Pages (from-to)	5-23
Journal	Formal methods in system design
Volume	18
Issue number	1
DOIs	https://doi.org/10.1023/A:1008736219484
Publication status	Published - 2001
Externally published	Yes

Keywords

n/a OA procedure

Access to Document

10.1023/A:1008736219484

Cite this

@article{0bcc106e6af64399970770d126828fa7,

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 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.",

keywords = "n/a OA procedure",

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

year = "2001",

doi = "10.1023/A:1008736219484",

language = "English",

volume = "18",

pages = "5--23",

journal = "Formal methods in system design",

issn = "0925-9856",

publisher = "Springer",

number = "1",

}

TY - JOUR

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

AU - Lind-Nielsen, Jørn

AU - Andersen, Henrik Reif

AU - Hulgaard, Henrik

AU - Behrmann, Gerd

AU - Kristoffersen, Kåre

AU - Larsen, Kim G.

PY - 2001

Y1 - 2001

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 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.

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 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.

KW - n/a OA procedure

U2 - 10.1023/A:1008736219484

DO - 10.1023/A:1008736219484

M3 - Article

SN - 0925-9856

VL - 18

SP - 5

EP - 23

JO - Formal methods in system design

JF - Formal methods in system design

IS - 1

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Cite this