Maude Specification of the MDS architecture and Examples

Grit Denker and Carolyn Talcott (SRI International)

Abstract:

Deep space missions are very expensive and involve complex and highly customized remote agent systems such as rovers or solar airplanes. Errors that surface during a mission usually imply major financial losses and in the worst case can result in a mission's failure. Methods that provide higher assurance of correctness, predictable behavior, and greater dependability of mission software are needed to reduce the risk of costly failure. The Mission Data System (MDS) has identified two key ideas for developing a remote agent system that will simplify and reduce the cost of design, test, and operation: (1) a state-based approach to system design; and (2) a goal-oriented approach to operation. The system state is the basis on which decisions about mission operations are based. Mission goals describe the desired outcome of a mission operation so that the overall mission will be successfully completed. Goal-oriented operation allows tasks to be described in terms of ``what'' rather than ``how.'' High-level goals are elaborated into flexible goal nets that combine lower-level goals.

The Formal Checklists for Remote Agents Dependability project will develop a formal basis, tools, and methods for enhancing dependability of goal-based operation of space missions. This includes a formal executable semantics for goal nets that is parametric in the domain model and can be instantiated to a wide range of domains; checklists of analysis tasks that assist in measuring the degree of dependability of a goal net; tools to mechanize and support the analysis tasks; and case studies for selected domain models to validate the formal framework and serve as a guide to its use. The resulting formal framework will allow certification to be added to reusability. Certified packages of goals, goal nets and corresponding software modules developed for one mission can be reused in future missions, supporting one of the objectives of remote agent architectures such as MDS that deep space missions are no longer one-of-a-kind, expensive engineering projects. This way mission systems not only become cheaper but also more reliable and the overall level of assurance of a mission's success is increased.

For more information see the related Formal Checklists for Remote Agent Dependability project.