Paper Info
Title
Early validation of requirements
Abstract
This paper describes a case study conducted to determine if formal methods could be used to validate system requirements early in the lifecycle atreasonable cost. Several hundred requirements for the mode logic of a typical Flight Guidance System were captured as natural language “shall” statements. A formal model of the mode logic was written in the RSML -e language and translated into the NuSMV model checker and the PVS theorem prover using translators developed as part of the project. Each “shall” statement was manually translated into a NuSMV or PVS property and proven using these tools.
Year
DOI
Venue
2004
10.1007/978-1-4020-8157-6_47
IFIP Congress Topical Sessions
Keywords
DocType
Citations 
theorem prover,natural language,formal method
Conference
0
PageRank 
References 
Authors
0.34
9
2
Name
Order
Citations
PageRank
Steven P. Miller156156.48
Mats P. E. Heimdahl256564.80