Specification, Synthesis and Verification of Software-based Control Protocols for Fault-Tolerant

Abstract

The demand for reliable and fault-tolerant space systems to deliver sophisticated missions under environmental factors changing over their operational lifespan is increasing their complexity and development costs. These systems are increasingly governed by software-based protocols, both onboard and on the ground, in addition to the conventional physical constraints and actuation and sensing limitations. The interactions between software-based protocols and the underlying physical components call for new methods and tools for the design of complex space systems and for affordably building assurance in their operation. The objective of this proposal is to develop (i) formal specifications of correctness for software-based control protocols for space systems and (ii) model-based verification and correct-by-construction synthesis methods and tools against these specification. To facilitate initial progress, we focus on the correctness of mode switching sequences and logics, reconfiguration strategies to recover from failures, automated debugging of such strategies, and systematic identification of the causes for failures.

Document Details

Document Type
DoD Grant Award
Publication Date
Jul 18, 2016
Source ID
FA94531510317

Entities

People

  • Ufuk Topcu

Organizations

  • Air Force Research Laboratory
  • United States Air Force
  • University of Texas at Austin

Tags

Fields of Study

  • Computer science
  • Engineering

Readers

  • Robotics and Automation.
  • Software Engineering.
  • Systems Analysis and Design

Technology Areas

  • Space
  • Space - Spacecraft Maneuvers