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

From Murray Wiki
Revision as of 05:39, 15 May 2016 by Murray (talk | contribs) (htdb2wiki: creating page for 2015f_mm15-aiaa.html)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search


Catharine L. McGhan and Richard M. Murray
AIAA Space 2015 Conference and Exposition

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.