Paper Info
Title
Analyzing tabular requirements specifications using infinite state model checking
Abstract
This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (software cost reduction) tabular notation using action language verifier (ALV). After reviewing the SCR method and tools and the action language, experimental results are presented of formally analyzing two SCR specifications using ALV, The application of ALV to verify or falsify (by generating counterexamples) the state and transition invariants of SCR specifications and to check disjointness and coverage properties is described. ALV is compared with the verification techniques that have been integrated into the SCR toolset.
Year
DOI
Venue
2006
10.1109/MEMCOD.2006.1695895
MEMOCODE
Keywords
Field
DocType
action language verifier,disjointness property,software cost reduction,coverage property,formal analysis,requirements specifications,infinite state model checking,tabular requirements specification,control systems,formal specification,air traffic control,formal languages,thyristors,application software,model checking,creep,software verification and validation,power generation,action language
Notation,Programming language,Formal language,Computer science,Action language,Real-time computing,Formal specification,Theoretical computer science,Counterexample,Application software,Software verification and validation,Cost reduction
Conference
ISBN
Citations 
PageRank 
1-4244-0421-5
2
0.47
References 
Authors
19
2
Name
Order
Citations
PageRank
Tevfik Bultan12481157.95
Constance L. Heitmeyer2898151.71