|
Static Analysis of Software for Autonomous Spacecrafts
|
|
Point of Contact
|
Supratik Mukhophadyay
Supratik.Mukhophadyay@mail.wvu.edu
|
|
Dates
|
January 2003 - December 2005
|
|
Problem
|
As NASA's missions continue to explore Mars and beyond, the great distances from Earth will require that they will be able to perform many of their tasks autonomously. While autonomy offers promises of improved capabilities at a reduced operational cost, development and validation of software for such autonomous spacecrafts poses a tough challenge. Traditional testing methods fall short of providing the desired confidence level due to the explosion in the number of possible situations. Formal verification methods not only suffer from the state explosion problem, but also require extraction of formal models from the software.
|
|
Objective
|
We intend to use static analysis techniques to analyze and validate software for autonomous systems. Such analysis can be applied at compile time without any need for extracting formal models from the code, and can be used to detect different types of bugs ranging from memory leaks to concurrency errors. The techniques developed will be implemented in a tool that will be loosely integrated with the compilers/interpreters. We intend to use as case studies the C++ version of Livingstone real time system health manager architecture (L2), the HSTS and the Smart Executive components (written in Lisp) of the Remote Agent autonomous spacecraft controller used in Deep Space 1 (DS1), the Fault Detection and Isolation Manager (FDIM), a standard command language (SCL) compatible derivative of Livingstone developed by the Interface and Control Systems Inc. as well as some hardware and software models encoded in the Model Programming Language (MPL).
|
|
Results
|
Development of toolkit.tar
|
|
Keywords
|
software safety, verification and validation, software testing
|
|
Categories
|
Domain-Specific Analysis
Static Analysis
|
|
