Formally verified run time assurance architecture of a 6U cubesat attitude control system

Kerianne H. Gross, Matthew A. Clark, Jonathan A. Hoffman, Aaron W. Fifarek, Kuldip S. Rattan, Eric D. Swenson, Michael W. Whalen, Lucas Wagner

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

3 Scopus citations


Intelligent controller designs based on artificial intelligence and machine learning promise superior performance over traditional control techniques; however, the lack of transparency in intelligent control systems and the opportunity for emergent behaviors limits where these systems may be applied. Run Time Assurance (RTA) is a proposed methodology to allow intelligent (unverified) controllers to perform within a predetermined envelope of acceptable behavior. Rather than depending entirely on offline verification, RTA provides an online verification approach. Based on the Simplex Architecture, RTA architectures use a decision module to monitor control system performance and switch control from an unverified controller to a verified backup controller if the unverified controller violates acceptable behavior ranges or is forced to operate outside of predetermined conditions. The focus of this work is to combine formal methods analysis with an RTA architecture to generate proof that the output of the RTA controller does not violate safety properties. A 6U CubeSat attitude control subsystem case study is presented and formal methods are used to prove the outputs of the verified controller, decision module, and the larger RTA control system never violate a set of safety properties describing actuator limitations.

Original languageEnglish (US)
Title of host publicationAIAA Infotech @ Aerospace Conference
PublisherAmerican Institute of Aeronautics and Astronautics Inc. (AIAA)
ISBN (Print)9781624103889
StatePublished - Jan 1 2016
EventAIAA Infotech @ Aerospace Conference, 2016 - San Diego, United States
Duration: Jan 4 2016Jan 8 2016

Publication series

NameAIAA Infotech @ Aerospace Conference


ConferenceAIAA Infotech @ Aerospace Conference, 2016
Country/TerritoryUnited States
CitySan Diego


Dive into the research topics of 'Formally verified run time assurance architecture of a 6U cubesat attitude control system'. Together they form a unique fingerprint.

Cite this