NASA Jet Propulsion Laboratory California Institute of Technology Follow this link to skip to the main content

BEACON eSpace at Jet Propulsion Laboratory >
JPL Technical Report Server >
JPL TRS 1992+ >

Please use this identifier to cite or link to this item:

Title: Validating Requirements for Fault Tolerant Systems Using Model Checking
Authors: Schneider, Francis
Easterbrook, Steve M.
Callahan, John R.
Holzlmann, Gerard J.
Issue Date: 6-Apr-1998
Citation: IEEE Computer Society
Colorado Springs, Colorado, USA
Abstract: Model checking is shown to be an effective tool in validating the behavior of a fault tolerant embedded spacecraft controller. The case study presented here shows that by judiciously abstracting away extraneous complexity, the state space of the model could be exhaustively searched allowing critical functional requirements to be validated down to the design level.
Appears in Collections:JPL TRS 1992+

Files in This Item:

File SizeFormat
97-1514.pdf247.58 kBAdobe PDFView/Open

Items in DSpace are protected by copyright, but are furnished with U.S. government purpose use rights.


Privacy/Copyright Image Policy Beacon Home Contact Us
NASA Home Page + Div 27
+ JPL Space
Site last updated on December 5, 2014.
If you have any comments or suggestions for this web site, please e-mail Robert Powers.