NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal Analysis of the Remote Agent Before and After FlightThis paper describes two separate efforts that used the SPIN model checker to verify deep space autonomy flight software. The first effort occurred at the beginning of a spiral development process and found five concurrency errors early in the design cycle that the developers acknowledge would not have been found through testing. This effort required a substantial manual modeling effort involving both abstraction and translation from the prototype LISP code to the PROMELA language used by SPIN. This experience and others led to research to address the gap between formal method tools and the development cycle used by software developers. The Java PathFinder tool which directly translates from Java to PROMELA was developed as part of this research, as well as automatic abstraction tools. In 1999 the flight software flew on a space mission, and a deadlock occurred in a sibling subsystem to the one which was the focus of the first verification effort. A second quick-response "cleanroom" verification effort found the concurrency error in a short amount of time. The error was isomorphic to one of the concurrency errors found during the first verification effort. The paper demonstrates that formal methods tools can find concurrency errors that indeed lead to loss of spacecraft functions, even for the complex software required for autonomy. Second, it describes progress in automatic translation and abstraction that eventually will enable formal methods tools to be inserted directly into the aerospace software development cycle.
Document ID
20000055731
Document Type
Conference Paper
Authors
Havelund, Klaus
(RECOM Technologies, Inc. Moffett Field, CA United States)
Lowry, Mike
(NASA Ames Research Center Moffett Field, CA United States)
Park, SeungJoon
(Research Inst. for Advanced Computer Science Moffett Field, CA United States)
Pecheur, Charles
(Research Inst. for Advanced Computer Science Moffett Field, CA United States)
Penix, John
(NASA Ames Research Center Moffett Field, CA United States)
Visser, Willem
(Research Inst. for Advanced Computer Science Moffett Field, CA United States)
White, Jon L.
(Caelum Research Corp. Moffett Field, CA United States)
Date Acquired
August 19, 2013
Publication Date
June 1, 2000
Publication Information
Publication: Lfm2000: Fifth NASA Langley Formal Methods Workshop
Subject Category
Computer Programming And Software
Distribution Limits
Public
Copyright
Public Use Permitted.
No Preview Available