Early validation of requirements: A case study using formal methods

Steven P. Miller, Mats P.E. Heimdahl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationBuilding the Information Society - IFIP 18th World Computer Congress Topical Sessions
PublisherSpringer New York LLC
Pages521-526
Number of pages6
ISBN (Print)1402081561, 9781402081569
StatePublished - Jan 1 2004
EventIFIP 18th World Computer Congress Topical Sessions - Toulouse, France
Duration: Aug 22 2004Aug 27 2004

Publication series

NameIFIP Advances in Information and Communication Technology
Volume156
ISSN (Print)1868-4238

Other

OtherIFIP 18th World Computer Congress Topical Sessions
CountryFrance
CityToulouse
Period8/22/048/27/04

Fingerprint Dive into the research topics of 'Early validation of requirements: A case study using formal methods'. Together they form a unique fingerprint.

Cite this