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.
This work is supported by NSF grant CCR-0234462.
| Documentation |
| Applications |
The formal specification of the MDS systems and application-layer adaptations is done using the Maude system. Maude is a high-performance reflective language and system supporting specification and analysis for a wide range of applications. Maude runs on many Unix variants, including Linux. It is provided free of charge under the terms of the GNU General Public License and can be downloaded at Maude download and installation.