Formally Verified Run Time Assurance Architecture of a 6U CubeSat Attitude Control System
| Autor: | Eric D. Swenson, Matthew Clark, Jonathan A. Hoffman, Aaron W. Fifarek, Michael W. Whalen, Lucas G. Wagner, Kuldip S. Rattan, Kerianne H. Gross |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
0209 industrial biotechnology
Engineering business.industry 020207 software engineering Control engineering 02 engineering and technology Transparency (human–computer interaction) Formal methods Attitude control 020901 industrial engineering & automation Backup Control theory Control system 0202 electrical engineering electronic engineering information engineering CubeSat business Envelope (motion) |
| Zdroj: | AIAA Infotech @ Aerospace. |
| DOI: | 10.2514/6.2016-0222 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|