Paper Info
Title
Applying infinite state model checking and other analysis techniques to tabular requirements specifications of safety-critical systems
Abstract
Although it is most often applied to finite state models, in recent years, symbolic model checking has been extended to infinite state models using symbolic representations that encode infinite sets. This paper investigates the application of an infinite state symbolic model checker called Action Language Verifier (ALV) to formal requirements specifications of safety-critical systems represented in the SCR (Software Cost Reduction) tabular notation. After reviewing the SCR method and tools, the Action Language for representing state machine models, and the ALV infinite state model checker, the paper presents experimental results of formally analyzing two SCR specifications using ALV. The application of ALV to verify or falsify (by generating counterexample behaviors) the state and transition invariants of SCR specifications and to check Disjointness and Coverage properties is described. The results of formal analysis with ALV are then compared with the results of formal analysis using techniques that have been integrated into the SCR toolset. Based on the experimental results, strengths and weaknesses of infinite state model checking with respect to other formal analysis approaches such as explicit and finite state model checking and theorem proving are discussed.
Year
DOI
Venue
2008
10.1007/s10617-008-9014-2
Design Automation for Embedded Systems
Keywords
Field
DocType
Infinite state model checking, Requirements specifications, Safety-critical systems
Notation,Model checking,Programming language,Life-critical system,Computer science,Action language,Automated theorem proving,Infinite set,Theoretical computer science,Finite-state machine,Counterexample
Journal
Volume
Issue
ISSN
12
1
1572-8080
Citations 
PageRank 
References 
3
0.42
34
Authors
2
Name
Order
Citations
PageRank
Tevfik Bultan12481157.95
Constance L. Heitmeyer2898151.71