Implementation of a Stochastic Timeline Validation Tool Integrated With R2U2

The Gateway Vehicle Systems Manager (VSM), the top-level software control system in a distributed, hierarchical Autonomous System Management Architecture, is operated using timelines generated on the ground and uplinked to the spacecraft. A timeline consists of a set of tasks that issue commands to internal VSM functions and external Module System Manager (MSM) functions. The tasks can include branching and conditional execution based on constraints. Tasks determine and report success/failure. It is essential that an uplinked timeline is free of real-time issues such as deadlocks and livelocks, does not violate resource or other constraints, completes each task within allocated durations, and is robust to uncertainty. In order to ensure that timelines don’t violate safety or other properties across the full set of feasible set of executions, numerous trial executions of the timeline are necessary and therefore, the simulation must be extremely time-efficient. The VSM team has developed a timeline validation tool (TVT) that uses discrete event simulation techniques. The tool queries mission databases and timeline files to automatically generate a Monte Carlo model of timeline execution. Model execution stochastically generates a set of event sequences which are in turn checked for violation of required properties using an offline version of the R2U2 runtime verifier.

This presentation describes the approach the VSM team has used to combine mission timeline files, mission databases, and a probability density function library to automatically produce an executable discrete event model, stochastically generate, and validate timeline execution sequences using R2U2:

1. Description of the timelines in the context of VSM operations
2. Description of the set of mission and supporting databases necessary to convert a timeline into an executable discrete event model
3. Incorporating probability density functions augmented with corner conditions for execution branch points, times of completion, resource consumption, and discrete branch outcomes
4. Executing Monte Carlo trials and recording for each trial an event sequence augmented with traceability metadata
5. Automatic generation of assume-guarantee contracts specific to each timeline that check for violation of critical properties
6. Integration of the timelines and assume-guarantee contracts with the validated runtime verification tool R2U2
7. Interpreting R2U2 verdict sequences and mapping failures to timeline tasks
8. Lessons learned and future work