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

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

    Research output: Contribution to journalJournal articleResearchpeer-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 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.
    Original languageEnglish
    JournalFormal Methods in System Design
    Volume18
    Issue number1
    Pages (from-to)5-23
    ISSN0925-9856
    DOIs
    Publication statusPublished - 2001

    Keywords

    • Formal verification
    • Symbolic model checking
    • Backwards reachability
    • Embedded software

    Fingerprint Dive into the research topics of 'Verification of Large State/Event Systems using Compositionality and Dependency Analysis'. Together they form a unique fingerprint.

    Cite this