NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Experiences Using Lightweight Formal Methods for Requirements ModelingThis paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies differ from previously reported applications of formal methods in that formal methods were applied very early in the requirements engineering process, to validate the evolving requirements. The results were fed back into the projects, to improve the informal specifications. For each case study, we describe what methods were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, formal methods enhanced the existing verification and validation processes, by testing key properties of the evolving requirements, and helping to identify weaknesses. We conclude that the benefits gained from early modeling of unstable requirements more than outweigh the effort needed to maintain multiple representations.
Document ID
19980016986
Document Type
Contractor Report (CR)
Authors
Easterbrook, Steve (West Virginia Univ. Fairmont, WV United States)
Lutz, Robyn (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA United States)
Covington, Rick (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA United States)
Kelly, John (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA United States)
Ampo, Yoko (Nippon Electric Co. Ltd. Tokyo, Japan)
Hamilton, David (Hewlett-Packard Co. San Diego, CA United States)
Date Acquired
September 6, 2013
Publication Date
October 16, 1997
Subject Category
Computer Programming and Software
Report/Patent Number
WVU-IVV-97-015
NASA/CR-1997-207044
WVU-CS-TR-97-017
NAS 1.26:207044
NASA-IVV-97-015
Funding Number(s)
CONTRACT_GRANT: NAS7-100
CONTRACT_GRANT: NCC2-979
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Available Downloads

NameType 19980016986.pdf STI