An Embeddable Virtual Machine for State Space Generation

M. Weber

doi:10.1007/978-3-540-73370-6_12

An Embeddable Virtual Machine for State Space Generation

M. Weber

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	Undefined
Title of host publication	Proceedings of the 14th International SPIN Workshop
Editors	D. Bosnacki, S. Edelkamp
Place of Publication	Berlin
Publisher	Springer
Pages	168-186
Number of pages	18
ISBN (Print)	978-3-540-73369-0
DOIs	https://doi.org/10.1007/978-3-540-73370-6_12
Publication status	Published - 2007
Event	14th International SPIN Workshop on Model Checking of Software 2007 - Berlin, Germany Duration: 1 Jul 2007 → 3 Jul 2007 Conference number: 14

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Number	Supplement
Volume	2595

Workshop

Workshop	14th International SPIN Workshop on Model Checking of Software 2007
Country	Germany
City	Berlin
Period	1/07/07 → 3/07/07

Keywords

EWI-11545
METIS-245852
IR-62050

Access to Document

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

http://eprints.eemcs.utwente.nl/secure2/11545/01/fulltext.pdf

Cite this

@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 ; null ; Conference date: 01-07-2007 Through 03-07-2007",

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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - An Embeddable Virtual Machine for State Space Generation

AU - Weber, M.

N1 - Conference code: 14

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

Y2 - 1 July 2007 through 3 July 2007

ER -