Formal Specification and Analysis of Spacecraft Collision Avoidance Run Time Assurance Requirements

Kerianne L. Hobbs, Jennifer Davis, Lucas Wagner, Eric Feron

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


One of the greatest challenges preventing the use of advanced controllers in aerospace is developing methods to verify, validate, and certify them with high assurance. One emerging approach is to push the burden of assurance from offline verification of an autonomous controller at design time, to online verification of safe behavior through a monitor and high assurance backup controller at run time. Run time assurance goes a step beyond alerting systems by detecting imminent unsafe behavior and intervening with a trusted control response. In the spacecraft domain, autonomous operations could be approved if run time assurance systems can provide collision avoidance capabilities. While several approaches to run time assurance have been developed and successfully demonstrated, the design and verification of these systems is ad hoc and specific to the application. This paper describes the elicitation, formal specification, and analysis of general collision avoidance system requirements for a conceptual spacecraft conducting autonomous close-proximity operations based on a run time assurance construct. This includes the first formally specified and analyzed generalized run time assurance architecture for spacecraft that includes a fault monitor, interlock monitor, and human-machine interface. Mathematically precise requirements are elicited through the process of formal specification based on common design elements, spacecraft guidance constraints in the literature, and a structured hazard assessment. Finally, the requirements are analyzed using compositional reasoning and formal model checking verification techniques.
Original languageEnglish (US)
Title of host publication2021 IEEE Aerospace Conference (50100)
ISBN (Print)9781728174365
StatePublished - Mar 6 2021

Bibliographical note

KAUST Repository Item: Exported on 2021-08-10


Dive into the research topics of 'Formal Specification and Analysis of Spacecraft Collision Avoidance Run Time Assurance Requirements'. Together they form a unique fingerprint.

Cite this