Discrete Event Simulation-Based Timeline Validation Using R2U2

The Gateway Vehicle Systems Manager (VSM), the top-level software control system in a distributed, hierarchical Autonomous System Management Architecture is, like most modern spacecraft software control systems, heavily data-driven. For example, schedules (timelines) will be developed on the ground and, due to the high degree of autonomy, contain complex procedures involving conditional branching, variable timing, and resource contention resolution. In order to verify that an uploaded timeline will function correctly, it is necessary to explore the feasible set of possible executions. While it is possible to test a timeline using a mission simulation, the complexity of the system and duration of a timeline limits the number of trials and therefore the test coverage. To address this problem, the VSM team is using a discrete event system model that can rapidly generate from a timeline sets of event sequences using Monte Carlo techniques. To achieve rapid and trustworthy checking of the event sequences, we use an offline version of the runtime model checking tool R2U2.

This presentation describes the approach the VSM team is using to implement the discrete event simulation and evaluate event sequences using R2U2. The presentation will discuss:
1. Description of the timelines by VSM in the context of VSM operations
2. Expansion of a timeline into a sequence of atomic events
3. Adjustment, in the Monte Carlo environment, of an event sequence to account for uncertainty, external events, and failures
4. Definition of R2U2 input and mission-time linear temporal logic files
5. Generation and use of R2U2 verdict sequences
6. Lessons learned and future work