Formal Checklists for Remote Agent Dependability

Sri International, Menlo Park CA

Investigators

Abstract

Talcott CCR-0234462 "FORMAL CHECKLISTS FOR REMOTE AGENT DEPENDABILITY" Deep Space Missions involve a tight integration of physical and software systems that must function autonomously over a prolonged time. These autonomous agents need to be robust and able to react in real time to state changes without aid of earth control. The Mission Data System (MDS) framework, consisting of an architecture, tools, and libraries of reusable components, has been developed by NASA to address this problem. This project builds on two key ideas of the MDS approach: a state-based approach to system design and a goal-oriented approach to operation. It develops a formal framework with methods and supporting tools for increasing the dependability of goal based operation of space systems. In particular, a formal approach to the analysis of goal net specifications is being developed that enables assertions to be made about their dependability level. A set of formal checklists (formal analysis suites) will be produced along with supporting tools that can be used to achieve more predictable dependability of goal nets and goal-based operation. The checklists will provide a qualitative means of measuring dependability of goal achievers. A spectrum of analysis techniques of different strengths will be developed to allow for achieving different levels of dependability. To experimentally validate the ideas, the framework will be applied to goal achievers for a representative set of domains in the context of the MDS test bed. The experimental work will guide the development of formal checklists. The resulting case studies will also serve as templates for further application of the formal framework. Certified packages of goals, goal nets and corresponding software modules developed for one mission can be re-used in future missions. The formal technology developed in this project will be applicable to a wide range of domains and physical situations.