Managing the Verification Trajectory


Ruys, T.C. and Brinksma, H. (2003) Managing the Verification Trajectory. International journal on software tools for technology transfer, 4 (2). pp. 246-259. ISSN 1433-2779

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking. Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem - which allows us to apply these techniques to ever larger systems - attention must now also be paid to the methodology of model checking, to decide how to use these techniques to their best advantage. Model checking "in the large" causes a substantial proliferation of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification process. We show that in order to do this well both notational and tool support are required. We discuss the use of software configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project, an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin.
Item Type:Article
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page