Julia M Badger | Engineering Papers

NASA NTRSDate not supplied

Adding a Verification View for Autonomous Real-Time Architecture

Spacecraft software systems continue to increase in complexity and must frequently operate autonomously for extended periods. Thus, the consequences of software flaws are increasing and it is necessary to improve development methods to minimize the risk of latent flaws in the operational software. Traditional software architectures place verification as one element in the development architectural view and treat verification as a later lifecycle activity that is considered complete when the system is certified for flight. The Gateway Vehicle System Manager team, recognizing the importance of verification throughout the system lifecycle, is treating verification as an additional architectural view that receives continuous attention from the requirements analysis phase and continuing for the life of the operational system. The verification view consists of two viewpoints: development and operational. We present background on the verification view and discuss the approaches the Vehicle System Manager team is taking.

James B Dabney↗

NASA NTRSDate not supplied

Using Assume-Guarantee Contracts in Autonomous Spacecraft

Explore the source record for details and available documents.

Verification and Validation↗

NASA NTRSDate not supplied

Stochastic Verification by Analysis for Autonomous Systems Management Architecture (ASMA)

The Gateway Vehicle Systems Manager (VSM) is the top-level of a distributed, hierarchical software control system. VSM is data-driven and will make decisions related to mission, fault, resource management and vehicle control. These attributes combined with a high degree of autonomy make it susceptible to emergent behavior. In order to achieve the high level of confidence needed in this critical system, the VSM team has developed a multifaceted verification strategy employing traditional verification techniques, simulation, model checking, and runtime verification. Individual algorithms are verified using conventional testing and model checking using assume-guarantee contracts. A discrete event-based simulation approach is being developed to verify timelines. This presentation describes an enhancement to the verification approach using analysis to enhance system robustness by detecting and resolving the potential for emergent behavior. The verification by analysis employs a Software in the Loop (SITL) environment with real flight software executing on emulated processors, simulations of vehicle subsystems, flight dynamics, and human inputs. Since the possible input space and configuration data set are too large for exhaustive testing, a Monte Carlo approach is used to cover feasible scenarios, augmented with corner cases and known higher-risk scenarios. A key problem in using Monte Carlo-based system verification is evaluating test results to ensure that system behavior is correct. The presentation describes the approach the VSM team uses to monitor behavior for compliance with predetermined boundaries and to identify anomalous behavior for further analysis. This presentation describes the multi-level systems approach to verification, and the simulation-based layer that covers the feasible state space: 1. Overview of the Gateway VSM 2. Special challenges due to heterogeneous, hierarchical architecture 3. Modeling and simulation environment using flight software and system simulations 4. Developing input sets to ensure state-space coverage 5. Developing model and data configuration sets to ensure model coverage 6. Interpreting results without predetermined outcomes 7. Lessons learned and future work

Verification and Validation↗