Managing the Verification Trajectory

T.C. Ruys, Hendrik Brinksma

    Research output: Contribution to journalArticleAcademicpeer-review

    8 Citations (Scopus)

    Abstract

    In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking. Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem - which allows us to apply these techniques to ever larger systems - attention must now also be paid to the methodology of model checking, to decide how to use these techniques to their best advantage. Model checking "in the large" causes a substantial proliferation of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification process. We show that in order to do this well both notational and tool support are required. We discuss the use of software configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project, an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin.
    Original languageUndefined
    Article number10.1007/s10009-002-0078-1
    Pages (from-to)246-259
    Number of pages14
    JournalInternational journal on software tools for technology transfer
    Volume4
    Issue number2
    DOIs
    Publication statusPublished - Feb 2003

    Keywords

    • IR-63270
    • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS
    • EWI-6405
    • FMT-MC: MODEL CHECKING

    Cite this