An embeddable virtual machine for state space generation

被引：2

作者：

Weber M. ^{[1
]}

机构：

[1] Formal Methods and Tools, University of Twente, Enschede

来源：

International Journal on Software Tools for Technology Transfer | 2010年 / 12卷 / 02期

关键词：

Model checking; Operational semantics; Promela; State space generation; Virtual machine;

D O I：

10.1007/s10009-010-0141-2

中图分类号：

学科分类号：

摘要：

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. © Springer-Verlag 2010.

引用

页码：97 / 111

页数：14

共 35 条

[1]

Barnat J., Brim L., Cerna I., Simecek P., DiVinE the distributed verification environment, 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'05), (2005)

[2]

Barnat J., Brim L., Rockai P., Scalable multi-core LTL model-checking, Bosnacki and Edelkamp [6], pp. 187-203, (2007)

[3]

Barnat J., Brim L., Simecek P., Weber M., Revisiting resistance speeds up I/O-efficient LTL model checking, TACAS, Vol. 4963 of Lecture Notes in Computer Science, pp. 48-62, (2008)

[4]

Bevier W., Towards an operational semantics of PROMELA in ACL2, Proceedings of the 3rd International SPIN Workshop, (1997)

[5]

Bolognesi T., Brinksma E., Introduction to the ISO specification language LOTOS, The Formal Description Technique LOTOS, pp. 23-73, (1989)

[6]

Model Checking Software, 4595, (2007)

[7]

Brat G., Havelund K., Park S., Visser W., Java PathFinder-second generation of a Java model checker, Proceedings of the Workshop on Advances in Verification, (2000)

[8]

Brim L., Distributed verification: Exploring the power of raw computing power, Formal Methods: Applications and Technology, Vol. 4346 of Lecture Notes in Computer Science, pp. 23-34, (2006)

[9]

de Villiers P., Visser W., ESML-a validation language for concurrent systems, 7-th Southern African Computer Symposium, pp. 59-64, (1992)

[10]

Dill D., Drexler A., Hu A., Yang C., Protocol verification as a hardware design aid, ICCD '92: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer and Processors, pp. 522-525, (1992)

← 1 2 3 4 →