An Embeddable Virtual Machine for State Space Generation

M. Weber

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    10 Citations (Scopus)

    Abstract

    The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages. Several tools have been built on top of the VM implementation we developed, to evaluate the benefits of the proposed approach.
    Original languageUndefined
    Title of host publicationProceedings of the 14th International SPIN Workshop
    EditorsD. Bosnacki, S. Edelkamp
    Place of PublicationBerlin
    PublisherSpringer
    Pages168-186
    Number of pages18
    ISBN (Print)978-3-540-73369-0
    DOIs
    Publication statusPublished - 2007
    Event14th International SPIN Workshop on Model Checking of Software 2007 - Berlin, Germany
    Duration: 1 Jul 20073 Jul 2007
    Conference number: 14

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    NumberSupplement
    Volume2595

    Workshop

    Workshop14th International SPIN Workshop on Model Checking of Software 2007
    CountryGermany
    CityBerlin
    Period1/07/073/07/07

    Keywords

    • EWI-11545
    • METIS-245852
    • IR-62050

    Cite this

    Weber, M. (2007). An Embeddable Virtual Machine for State Space Generation. In D. Bosnacki, & S. Edelkamp (Eds.), Proceedings of the 14th International SPIN Workshop (pp. 168-186). [10.1007/978-3-540-73370-6_12] (Lecture Notes in Computer Science; Vol. 2595, No. Supplement). Berlin: Springer. https://doi.org/10.1007/978-3-540-73370-6_12