Sciweavers

Share
SPIN
2007
Springer

An Embeddable Virtual Machine for State Space Generation

10 years 9 months ago
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.
Michael Weber
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where SPIN
Authors Michael Weber
Comments (0)
books