Formal Checklists for Remote Agent Dependability

TalcottCCR-0234462“远程代理可靠性正式核对表”深空任务涉及物理和软件系统的紧密集成，这些系统必须在较长时间内自主运行。这些自主代理需要健壮，并能够在不借助地球控制的情况下对状态变化做出实时反应。美国宇航局为解决这一问题开发了飞行任务数据系统(MDS)框架，该框架由一个架构、工具和可重复使用的组件库组成。该项目建立在MDS方法的两个关键思想之上：基于状态的系统设计方法和面向目标的操作方法。它制定了一个正式框架，其中包括提高空间系统基于目标的操作的可靠性的方法和辅助工具。特别是，正在制定一种分析目标网规格的正式方法，以便能够对其可靠性水平作出断言。将编制一套正式清单(正式分析套件)以及可用于实现目标网和基于目标的行动的更可预测的可靠性的支持工具。核对表将提供一种衡量目标成功者可靠性的定性方法。将开发一系列不同强度的分析技术，以实现不同级别的可靠性。为了从实验上验证这些想法，该框架将在MDS试验台的上下文中应用于一组具有代表性的领域的目标成就者。试验性工作将指导制定正式的核对表。由此产生的案例研究也将作为进一步应用正式框架的模板。为一个特派团开发的经认证的一揽子目标、目标网和相应的软件模块可在今后的特派团中重复使用。该项目开发的正式技术将适用于广泛的领域和物理情况。

TalcottCCR-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.