A Caltech Library Service

Application of Correct-by-Construction Principles for a Resilient Risk-Aware Architecture

McGhan, Catharine L. R. and Murray, Richard M. (2015) Application of Correct-by-Construction Principles for a Resilient Risk-Aware Architecture. In: AIAA SPACE 2015 Conference and Exposition. Vol.Art. No. 24. AIAA , Reston, VA. ISBN 978-1-62410-334-6.

[img] PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


In this paper we discuss the application of correct-by-construction techniques to a resilient, risk-aware software architecture for onboard, real-time autonomous operations. We mean to combat complexity and the accidental introduction of bugs through the use of verifiable auto-coding software and correct-by-construction techniques, and discuss the use of a toolbox for correct-by-construction Temporal Logic Planning (TuLiP) for such a purpose. We describe some of TuLiP’s current functionality, specifically its ability to model symbolic discrete systems and synthesize software controllers and control policies that are correct-by-construction. We then move on to discuss the use of these techniques to define a deliberative goal-directed executive capability that performs risk-informed action-planning – to satisfy the mission goals (specified by mission control) within the specified priorities and constraints. Finally, we discuss an application of the TuLiP process to a simple rover resilience scenario.

Item Type:Book Section
Related URLs:
URLURL TypeDescription
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2015 AIAA. The authors would like to thank Tiago Vaquero and Klaus Havelund for their help as sounding boards during the problem formulation process, and Scott Livingston for his help in understanding the capabilities of the TuLiP and gr1c software algorithms. The authors would also like to thank both the Model-based Embedded Robotic Systems Group at MIT, and Michel Ingham and the System Architectures and BehaviorsGroup at the NASA Jet Propulsion Lab for their input and feedback during the development process. We would also like to thank the Keck Institute of Space Studies for its initial study and final report on Engineering Resilient Space Systems, from which this effort has originated. The research described in this paper was carried out at the California Institute of Technology under a grant from the Keck Institute for Space Studies.
Group:Keck Institute for Space Studies
Funding AgencyGrant Number
Keck Institute for Space Studies (KISS)UNSPECIFIED
Other Numbering System:
Other Numbering System NameOther Numbering System ID
AIAA Paper2015-4527
Record Number:CaltechAUTHORS:20160404-092715239
Persistent URL:
Official Citation:Catharine L. McGhan and Richard Murray. "Application of Correct-by-Construction Principles for a Resilient Risk-Aware Architecture", AIAA SPACE 2015 Conference and Exposition, SPACE Conferences and Exposition, (AIAA 2015-4527).
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:65888
Deposited By: Colette Connor
Deposited On:04 Apr 2016 17:29
Last Modified:10 Nov 2021 23:50

Repository Staff Only: item control page