An embeddable virtual machine for state space generation |
| |
Authors: | Michael Weber |
| |
Affiliation: | 1. Formal Methods and Tools, University of Twente, Enschede, The Netherlands
|
| |
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 around the VM implementation we developed, to evaluate the benefits of the proposed approach. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|