@inproceedings{4c9d8e08cdc84a94bc8610ea55de382a,
title = "Early validation of requirements: A case study using formal methods",
abstract = "This paper describes a case study conducted to determine if formal methods could be used to validate system requirements early in the lifecycle at reasonable 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.",
author = "Miller, {Steven P.} and Heimdahl, {Mats P.E.}",
year = "2004",
month = jan,
day = "1",
language = "English (US)",
isbn = "1402081561",
series = "IFIP Advances in Information and Communication Technology",
publisher = "Springer New York LLC",
pages = "521--526",
booktitle = "Building the Information Society - IFIP 18th World Computer Congress Topical Sessions",
note = "IFIP 18th World Computer Congress Topical Sessions ; Conference date: 22-08-2004 Through 27-08-2004",
}