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.