Early Validation of Requirements
Steven Paul Miller, Mats P. E. Heimdahl · 2008
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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.