An Object-Oriented Framework for Explicit-State Model Checking

M. Kattenbelt, T.C. Ruys, Arend Rensink

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    21 Downloads (Pure)

    Abstract

    This paper presents a conceptual architecture for an object-oriented framework to support the development of formal veri��?cation tools (i.e. model checkers). The objective of the architecture is to support the reuse of algorithms and to encourage a modular design of tools. The conceptual framework is accompanied by a C++ implementation which provides reusable algorithms for the simulation and veri��?cation of explicit-state models as well as a model representation for simple models based on guard-based process descriptions. The framework has been successfully used to develop a model checker for a subset of PROMELA.
    Original languageEnglish
    Title of host publicationProceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007)
    EditorsP. Groot, A. Serebrenik, M. van Eekelen
    Place of PublicationEindhoven
    PublisherEindhoven University of Technology
    Pages84-92
    Number of pages9
    Publication statusPublished - 23 Mar 2007

    Publication series

    NameTUE Computer Science Reports
    PublisherEindhoven University of Technology (TUE)
    Number07-04
    ISSN (Print)0926-4515

    Keywords

    • FMT-MC: MODEL CHECKING
    • METIS-255889
    • IR-65394
    • EWI-15091

    Fingerprint Dive into the research topics of 'An Object-Oriented Framework for Explicit-State Model Checking'. Together they form a unique fingerprint.

  • Cite this

    Kattenbelt, M., Ruys, T. C., & Rensink, A. (2007). An Object-Oriented Framework for Explicit-State Model Checking. In P. Groot, A. Serebrenik, & M. van Eekelen (Eds.), Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007) (pp. 84-92). (TUE Computer Science Reports; No. 07-04). Eindhoven: Eindhoven University of Technology.