Tags:Assume/Guarantee Contracts, Model checking and Trusted autonomy
Abstract:
The Vehicle System Manager (VSM) is the highest-level software control system in the Gateway hierarchical Autonomous System Management Architecture (ASMA). A key objective in ASMA design is to focus on infrastructure and systems to allow autonomous operations aboard Gateway. VSM will integrate modules and visiting vehicles to assist ground controllers and onboard crew in operation of Gateway as the head of a distributed and hierarchical system. VSM provides four function categories: Mission Management and Timeline Execution, Resource Management, Fault Management, Vehicle Control and Operation. VSM provides levels of automation ranging from fully autonomous operations with no flight crew and minimal ground monitoring to advisory automation when Gateway is crewed and has full ground monitoring. Trustworthiness is achieved via verified specification, comprehensive development verification, and real-time verification using assume-guarantee contracts (AGCs). Development verification includes semantic verification of the data model via peer review and testing. Development AGCs are implemented using the PlusCal/TLA+ environment to model key state machines with AGCs implemented as assertions and linear temporal logic formulas, driving model checker TLC. VSM uses runtime AGCs, implemented in R2U2 using assertions in propositional logic and guarantees in mission-time linear temporal logic. R2U2 permits formulas to be written in a mathematically concise, unambiguous notation. Additionally R2U2 is optimized for speed and size and the inferencing engine has been proven correct with respect to the operator space. R2U2 is integrated in VSM via a runtime monitor that feeds the necessary telemetry data to R2U2 and which receives and responds to the R2U2 verdict stream. The full lifecycle verification approach and use of AGCs provides increased trustworthiness to VSM. Preliminary results provide encouragement that VSM can be both autonomous and trustworthy.
Trustworthy Autonomy for Gateway Vehicle System Manager