Skip past navigation NASA Langley Formal Methods



quick page




  home > research > fm-savh

Spacecraft Autonomy and AI Planning

One of the main obstacles hindering the adoption of autonomous software for man-rated critical applications is the lack of a rigorous means of establishing the safety of these systems. Although AI-based autonomous software can provide enormous capability and flexibility, this power comes at a price: the verification and validation problem is greatly exacerbated. Traditional simulation based testing methods fall short of providing the needed level of confidence level. In other application domains, formal methods have been developed which explore the entire state space of the application providing rigorous guarantees about critical safety properties of the application. Unfortunately little progress has been made to date in applying formal methods to AI-based autonomous software systems. Some ground breaking work has been made by Charles Pecheur of NASA Ames [1,2,3] , but there are huge challenges in making techniques such as these practical for the system being developed under the Spacecraft Autonomy for Vehicles and Habitats Project. In [2] Menzies and Pecheur write
    The main challenge in verifying AI software (or, for that matter, any kind of complex system) comes from the number of different possible executions that have to be taken into account. We refer broadly to this uncertainty on a system's future behavior as non-determinism. Non-deterministic choices come from incoming external events, scheduling of concurrent tasks, or even intentional random choices in the program, to name a few. Every choice point in the execution results in as many possible subsequent execution branches. Typically, those choices compound into exponentially many possible executions. This is known as the state space explosion phenomenon.

Plan Verification

Procedure Representation Language (PRL)

Plan Execution Interchange Language (PLEXIL)

Note: The link to external site tag identifies links that are outside of the NASA domain.


Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 26 September 2003 (10:10:40)