# Presentation: 066136

## Verifying AI Plan ModelsEven the best laid plans need to be verified

- Margaret Smith – PI
- Gordon Cucullu
- Gerard Holzmann
- Benjamin Smith

- Prepared for the 2004
- Software Assurance
- Symposium (SAS)

**DS1**

**MSL**

**MSL**

## Problem

- How do you know that an Artificial Intelligence (AI) Onboard Planner will produce only *good* plans when it is flown?

**goals**

**state**
**variables**

**resources**

**activities**

- AI Planner

- Input
- model

**Plans**

- Once the planner selects a plan, with a simple check we can show that the *plan* is consistent with the *input model* provided to the planner.
- But there is currently no method to check that the *input model* will allow only *good* plans.

## Problem, 2How are AI models tested currently?

- Construct the model from Science or other requirements.
- Inspect the model for correctness against requirements.
- Input the model to the AI planner and ask for a specified number of plans.
- Manually inspect plans to identify bad plans

- Adjust constraints and other model elements to exclude bad plans.

**  ****bad**
**plan(s)**

**all good**
**plans(s)**

- End testing

**  ****try again**

## Approach

- Test plan models **exhaustively** to determine whether an *input model* allows bad plans.

- Construct the model from Science or other requirements.
- Inspect the model for correctness against requirements.
- Formulate ‘good plan’ properties
- Express model in Promela and **exhaustively check** using Spin.

- Adjust constraints and other model elements to exclude bad plans.

**  ****bad plan**
** ****(error trace)**

**no errors**

- End testing

**  ****try again**

## Benefits

- Retire an important class of risks inherent to all missions using AI Planners.
- by replacing a *sampling *test method with an *exhaustive* test method
- Enable autonomous systems that are needed by NASA projects to meet budget and science return requirements.

## Relevance to NASA

- High mission operations costs are pushing NASA funded missions toward more autonomous planning capabilities.
- Communication delays for Deep Space missions are a poor match with traditional commanded spacecraft.

- Methods for testing must keep pace with the highly complex, autonomous systems we are developing.

## Accomplishments

- Work on this project began in January, 2004.
- Team members (Affiliation: JPL):
- Margaret Smith (PI) – model checking, property specification
- Gordon Cucullu – model checking, spacecraft domain expert
- Gerard Holzmann – author of the Spin model checker, model checking expert
- Ben Smith – member of the JPL AI community, AI expert

## Accomplishments, 2

- Scoped the problem: worked with the JPL AI community to identify an important class of risks associated with AI planners.
- The risk identified is that *AI input models*, which are built by hand, may permit a AI planner to select a *bad* plan.
- Using ‘toy’ problems, demonstrated that the Spin model checker can find *bad* plans allowed by the input model.
- The *input model* is expressed in Promela, the language of the Spin model checker.
- A *good* plan is expressed formally as a property
- Spin finds an exception to the good plan (i.e. a *bad* plan) and reports it as an error.

## Accomplishments, 3

- Using a real example, the now cancelled DS4/ST4 Champollion mission, demonstrated that Spin can find *bad* plans on real AI input models.
- The model, when expressed in Promela, is tractable (can be exhaustively checked within memory constraints of a desktop PC with 2 GB of memory in a few minutes).
- We analyzed the bad plan produced by Spin, and fixed the AI input model, by adding a missing constraint.
- An exhaustive recheck with Spin showed that the fixed model can only produce good plans.

## Next Steps

- Test additional properties of the DS4/ST4 input model.
- Repeat the process on other AI models we have acquired to see if we get similar positive results.
- Repeat the process recently launched or soon to be launched missions:
- Earth Orbiter 1
- 3 Corner Sat