10.2514/6.2016-0222">
 

Formally Verified Run Time Assurance Architecture of a 6U CubeSat Attitude Control System

Document Type

Conference Proceeding

Publication Date

1-4-2016

Abstract

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.

Comments

Session: Software Architecture and Robust Software Engineering

This conference paper is published by AIAA and is available by subscription or purchase at the DOI link below.

Source Publication

AIAA Infotech @ Aerospace

Link to Full Text

Share

COinS