NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Implementation of a Stochastic Timeline Validation Tool Integrated With R2U2The 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
Document ID
20260001114
Acquisition Source
Johnson Space Center
Document Type
Presentation
Authors
James B Dabney
(University of Houston - Clear Lake Houston, United States)
Michael Whitzer
(Johnson Space Center Houston, United States)
Pavan Rajagopal
(CACI International (United States) Arlington, United States)
Snigdha Palamari
(CACI International (United States) Arlington, United States)
Sonali Thakkar
(CACI International (United States) Arlington, United States)
Chris Pohlen
(Amentum Chantilly, Virginia, United States)
Hemanth Koralla
(Amentum Chantilly, Virginia, United States)
Andrew Albright
(METECS Houston, Texas, United States)
Jeremy D. Frank
(Ames Research Center Mountain View, United States)
Date Acquired
February 5, 2026
Publication Date
March 23, 2026
Publication Information
Publisher: National Aeronautics and Space Administration
Subject Category
Computer Programming and Software
Meeting Information
Meeting: 19th Annual Workshop on Spacecraft Flight Software (FSW)
Location: Laurel, MD
Country: US
Start Date: March 23, 2026
End Date: March 26, 2026
Sponsors: The Aerospace Corporation, Southwest Research Institute, The Johns Hopkins University Applied Physics Laboratory, National Aeronautics and Space Administration, Jet Propulsion Laboratory
Funding Number(s)
CONTRACT_GRANT: 80JSC025D0071
CONTRACT_GRANT: 80JSC022DA035
WBS: 651937.06.03.72
CONTRACT_GRANT: 80JSC023DA010
Distribution Limits
Public
Copyright
Public Use Permitted.
Keywords
Verification
Formal Methods
No Preview Available