# Presentation: 126597

## Validating the Remote Agent Experiment for Spacecraft Autonomy

- Ben Smith1, Bill Millar2, Julia Dunphy1, Yu-Wen Tung1,
- Pandu Nayak2, Ed Gamble1, Micah Clark1

- Jet Propulsion Laboratory1
- NASA Ames Research Center2

## First mission of the New Millennium Program

**image courtesy JPL**

- Will validate12 new technologies
- Solar Electric Propulsion (SEP)
- On-board optical navigation
***Remote Agent Experiment*** 			(operates s/c autonomously for 6 days)
- Demonstrating a scalable validation approach for RA will be critical for using autonomy on future missions.

## Remote Agent vs. Traditional FSW:Operations and Testing

- Traditional
- Time-tagged sequences
- single execution path
- can test prior to execution
- Fail-safe
- abort sequence and safe s/c
- test ea. response in isolation

- RAX
- Goal-based commanding
- expands goals into plans onboard
- Fail-operational
- recovers plan or replans
- recovery affects future activities.
- Behavior conditional on goals and s/c responses.
- Many possible execution paths.

## Validation Challenges & Approaches

- Challenges
- Need high confidence in RAX for all scenarios
- Scarce Testing Resources (workforce & testbeds)
- Approach
- Parameter-based Testing around nominal baseline
- Design tests to exploit lower-fidelity test beds.
- Automated Verification tools

## Testing around a Baseline

- Map input space to parameter space
- Partition values of ea. param into equiv. classes to reduce space to manageable size. (*ad hoc*)
- Test all 1-parameter variations from baseline
- Shows impact of each parameter value in isolation.
- Test multiple-variations from baseline
- Test parameter combinations based on design
- Test all pairs of parameter values [e.g., Cohen, 1989]

## Orthogonal Array (All Pairs)

## Testing around Baseline:Applicability Assumptions

- There is a baseline scenario expected in flight
- good assumption for RAX and most science missions.
- Changes to baseline during flight unlikely.
- Can expect isolated changes.
- Changes to baseline before flight more likely.
- Baseline changes slowly.
- Tests should cover most probable changes.

## Exploiting Low-fidelity Testbeds

- Need to use low-fidelity testbeds
- More abundant, faster, more configurable
- Need extrapolation argument
- why does tested behavior hold w/ higher fidelity.
- RAX reasons about s/c as seen through FSW
- Reasoning is unaffected by increasing fidelity.
- Range of s/c behaviors same for low/hi fidelity sims.
- CPU resources, exact s/c behavior affected by fidelity.

## Assigning Tests to Testbeds

- Verify most requirements on low-fidelity testbeds
- Verify RAX reasoning on range of s/c behaviors
- Easier to control s/c behavior with low-fidelity sims
- Testbeds are faster: can run more tests.
- Catches the most obvious bugs early.
- Spot-check on higher fidelity testbeds
- Run just a few (~10) system-level tests
- Check performance and exact s/c behavior
- Rely on low-fidelity tests for depth of coverage.

## Verification Tools

- Plan-checker
- verifies correctness of plan wrt planner model
- verifies correctness of plan wrt requirements in first-order predicate logic (FOPL).
- Exec-view
- Display plan execution intuitively and highlight key aspects. Vastly easier than verifying from logs.
- Flight-rule checker
- Convert execution trace to sequence and verify through SEQGEN (tool that verifies all DS1 sequences).

## Plan Checker

- Requirements

- Plan Model

- Fact-base

- FOPL statements

- Plan contains one
**mm-update **token at time *t*.

**turning-on **meets **micas-on**

**R2: **$ *x *(and (start-time *x* t)
-                      (tk-type *x*
*	**    * **mm-update**))

**R1:** "*x* (tk-type *x* **turning-on**)
-        implies
-        $*y* (and (tk-type *y* **micas-on**)
-                     (meets *x y*))

- Plan

- Turn-on

- micas-on

- Mm-update

- Turn-on

- image

- image

- contains

- t

- (tk-type t1 turn-on)
- (tk-type t2 turn-on)
- (tk-type t3 micas-on)
- (tk-type t4 mm-update)
- (meets t1 t2)
- (meets t2 t3) . . .

- Report

- R1: FAIL
-   x=t1: Ø$y that sat. R1
-   x=t2:  sat. by y=t3
- R2: PASS
-   sat by x=t4

## Status and Results

- Completed low-fidelity testing (Unix/PPC)
- caught and fixed ~600 bugs
- Initial medium-fidelity testing (Papabed)
- caught ~20 bugs dealing with performance, exact FSW and s/c behavior.
- Extrapolation arguments are holding
- Beginning high-fidelity testing (DS1 Testbed)

## Conclusions

- Testing around baseline effective approach for RAX.
- Larger test-suites and small test teams introduce need for:
- S/W design that can exploit lower fidelity testbeds.
- Automated verification tools.
- Successful demonstration of RAX validation methods will help pave the way for spacecraft autonomy on future missions.

## Backup Slides

## TESTING

- PROCEDURE

## Traditional FSW

- Traditional Commanding
- FSW provides library of commands
- Execute time-tagged sequences of commands
- Traditional Verification and Validation
- Verify FSW using standard methods
- Verify and validate each sequence prior to execution by executing it on the testbed.

## Test Generation:Default Testing (“Single Variation”)

- Map input space (scenarios) to parameter space
- each parameter has several values
- Partition values of ea. param into equiv. classes to reduce space to manageable size. (*ad hoc*)
- Test *every* change of 1 param-value off baseline
- Shows impact of each parameter value in isolation.
- Usually manageable number of cases (# param values)
- Tests all single-anomaly cases off the baseline.
- Good for testing impact of in-flight anomalies.

## Test Generation:Multiple Variations

- Vary several parameters from baseline in each test
- Good for testing multi-faults in-flight and changes to baseline pre-flight.
- Select parameter combinations based on design
- params that are expected to interact
- Select all pairs of parameter values
- Empirically provides good code coverage. [cite]
- Orthogonal-arrays generate minimal suites. [cite]
- Both of above

## RAX Test Suites

- Planner:
- inputs = baseline goals, on-board goals, s/c state
- default testing + all-pairs around baseline + selected
- MIR
- inputs = monitor inputs, last Exec command.
- default testing + selected multi-variation
- Exec: execute PS/MIR scenarios
- System: selected off-nominal scenarios.

## DS1 Testbeds

## Formal Methods

- Formal methods provide very high confidence
- e.g., prove that models and engines are correct wrt requirements
- Desirable for missions that make full use of autonomy.
- Methods still need to be designed
- Performed a few feasibility studies on RAX.
- Validate parts of Exec w/ SPIN [Lowry *et al.*, 97]
- Validate toy planner models [Lowry *et al.*, 98]