Formal Checklists for Remote Agent Dependability

Remote agents used in Deep Space Missions such as rovers or solar airplanes must function autonomously over a prolonged time during planetary exploration. The Mission Data System (MDS) framework has been developed to address design and deployment of these complex systems. We are using the Maude environment to develop a formal framework with methods and supporting tools for increasing the dependability of MDS space systems. This is done by developing formal executable specifications of the MDS framework and its mission-specific adaptations and providing a set of formal checklists (formal analysis suites) that can be used to achieve better predictability and dependability. In this paper we present our formal model of the MDS framework, an adaptation for a remote rover and preliminary checklists for remote agents.