Abstract
| 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 | |
| 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
Cite this
}
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 - 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 -