Managing the Verification Trajectory

T.C. Ruys, Hendrik Brinksma

Research output: Contribution to journalArticleAcademicpeer-review

8 Citations (Scopus)

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.
Original languageUndefined
Article number10.1007/s10009-002-0078-1
Pages (from-to)246-259
Number of pages14
JournalInternational journal on software tools for technology transfer
Volume4
Issue number2
DOIs
Publication statusPublished - Feb 2003

Keywords

  • IR-63270
  • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS
  • EWI-6405
  • FMT-MC: MODEL CHECKING

Cite this

@article{20cc4e93400c4fcba58d31e3c3e2b891,
title = "Managing the Verification Trajectory",
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.",
keywords = "IR-63270, FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS, EWI-6405, FMT-MC: MODEL CHECKING",
author = "T.C. Ruys and Hendrik Brinksma",
year = "2003",
month = "2",
doi = "10.1007/s10009-002-0078-1",
language = "Undefined",
volume = "4",
pages = "246--259",
journal = "International journal on software tools for technology transfer",
issn = "1433-2779",
publisher = "Springer",
number = "2",

}

Managing the Verification Trajectory. / Ruys, T.C.; Brinksma, Hendrik.

In: International journal on software tools for technology transfer, Vol. 4, No. 2, 10.1007/s10009-002-0078-1, 02.2003, p. 246-259.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Managing the Verification Trajectory

AU - Ruys, T.C.

AU - Brinksma, Hendrik

PY - 2003/2

Y1 - 2003/2

N2 - 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.

AB - 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.

KW - IR-63270

KW - FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

KW - EWI-6405

KW - FMT-MC: MODEL CHECKING

U2 - 10.1007/s10009-002-0078-1

DO - 10.1007/s10009-002-0078-1

M3 - Article

VL - 4

SP - 246

EP - 259

JO - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

SN - 1433-2779

IS - 2

M1 - 10.1007/s10009-002-0078-1

ER -