This paper presents a conceptual architecture for an object-oriented framework to support the development of formal veri��?cation tools (i.e. model checkers). The objective of the architecture is to support the reuse of algorithms and to encourage a modular design of tools. The conceptual framework is accompanied by a C++ implementation which provides reusable algorithms for the simulation and veri��?cation of explicit-state models as well as a model representation for simple models based on guard-based process descriptions. The framework has been successfully used to develop a model checker for a subset of PROMELA.
|Title of host publication||Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007)|
|Editors||P. Groot, A. Serebrenik, M. van Eekelen|
|Place of Publication||Eindhoven|
|Publisher||Eindhoven University of Technology|
|Number of pages||9|
|Publication status||Published - 23 Mar 2007|
|Name||TUE Computer Science Reports|
|Publisher||Eindhoven University of Technology (TUE)|
- FMT-MC: MODEL CHECKING
Kattenbelt, M., Ruys, T. C., & Rensink, A. (2007). An Object-Oriented Framework for Explicit-State Model Checking. In P. Groot, A. Serebrenik, & M. van Eekelen (Eds.), Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007) (pp. 84-92). (TUE Computer Science Reports; No. 07-04). Eindhoven: Eindhoven University of Technology.