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.
|Name||TUE Computer Science Reports|
|Publisher||Eindhoven University of Technology (TUE)|
|Other||3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007)|
|Period||23/03/07 → 23/03/07|
|Other||23 March 2007|
- FMT-MC: MODEL CHECKING