FORMID : A Formal Specification And Verification Environment For DREAMS

Abstract

This paper presents the work performed in the context of the MUROCO-II on-going project. It has as objective the implementation of a generic formal mission specification and verification tool, named FORMID, and its integration into the DREAMS ESA robotic ground control station ([1,2]), in order to support, the A&R activities specification, formal verification and execution for the AURORA Mars exploration missions. MUROCO-II is the continuation of the MUROCO-I ([3]) study that provided a formal approach to the instantiation of the ESA Functional Reference Model robot control architecture. It established the framework and the benefits of the use of modern techniques for formal specification and formal verification of robotic tasks and actions that coordinate the robot behaviour to achieve the objectives of a mission. In contrast to the current approaches of robot programming, where there is a lack of high level primitives to specify parallelism, concurrency and synchronisation and where the validation of the tasks is performed by simulation covering a limited number of possible scenarios, in this case complex behaviours can be easily specified and the validation is done using rigorous mathematical analysis of all the possible states of execution. The use of formally defined languages for the coordination of the behaviours is expected to significantly increase the possibility of specifying complex behaviours providing more autonomy capabilities and to drastically reduce the testing and debugging interval while it will highly improve our confidence on the uploaded code. The integration of FORMID into DREAMS and its customisation for Mars exploration missions offers a solid basis for the future ground control station of robotic exploration missions. This paper is structured as follows: first we present the MUROCO framework, then we provide a technical insight into FORMID and finally we present its integration into the DREAMS ground control station.