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
Weber, M. / An Embeddable Virtual Machine for State Space Generation. Proceedings of the 14th International SPIN Workshop. editor / D. Bosnacki ; S. Edelkamp. Berlin : Springer, 2007. pp. 168-186 (Lecture Notes in Computer Science; Supplement).
@inproceedings{37d110a9d17a4878905b1fe5636ccf2a,
title = "An Embeddable Virtual Machine for State Space Generation",
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.",
keywords = "EWI-11545, METIS-245852, IR-62050",
author = "M. Weber",
note = "10.1007/978-3-540-73370-6_12",
year = "2007",
doi = "10.1007/978-3-540-73370-6_12",
language = "Undefined",
isbn = "978-3-540-73369-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "Supplement",
pages = "168--186",
editor = "D. Bosnacki and S. Edelkamp",
booktitle = "Proceedings of the 14th International SPIN Workshop",

}

Weber, M 2007, An Embeddable Virtual Machine for State Space Generation. in D Bosnacki & S Edelkamp (eds), Proceedings of the 14th International SPIN Workshop., 10.1007/978-3-540-73370-6_12, Lecture Notes in Computer Science, no. Supplement, vol. 2595, Springer, Berlin, pp. 168-186, 14th International SPIN Workshop on Model Checking of Software 2007, Berlin, Germany, 1/07/07. https://doi.org/10.1007/978-3-540-73370-6_12

An Embeddable Virtual Machine for State Space Generation. / Weber, M.

Proceedings of the 14th International SPIN Workshop. ed. / D. Bosnacki; S. Edelkamp. Berlin : Springer, 2007. p. 168-186 10.1007/978-3-540-73370-6_12 (Lecture Notes in Computer Science; Vol. 2595, No. Supplement).

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

TY - GEN

T1 - An Embeddable Virtual Machine for State Space Generation

AU - Weber, M.

N1 - 10.1007/978-3-540-73370-6_12

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - EWI-11545

KW - METIS-245852

KW - IR-62050

U2 - 10.1007/978-3-540-73370-6_12

DO - 10.1007/978-3-540-73370-6_12

M3 - Conference contribution

SN - 978-3-540-73369-0

T3 - Lecture Notes in Computer Science

SP - 168

EP - 186

BT - Proceedings of the 14th International SPIN Workshop

A2 - Bosnacki, D.

A2 - Edelkamp, S.

PB - Springer

CY - Berlin

ER -

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