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

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


    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 languageEnglish
    Title of host publicationProceedings of TACAS'98 (LNCS 1384)
    PublisherSpringer Verlag
    Publication date1999
    Publication statusPublished - 1999
    EventTACAS 98 -
    Duration: 1 Jan 1997 → …


    ConferenceTACAS 98
    Period01/01/1997 → …

    Cite this