ABSTRACT
Purpose of the present study is to provide a formal approach for the instantiation of the ESA unctional Reference Model robot control architecture in support of A&R mars exploration missions where a colony of robots paves the way of human exploration programs. The accent here is to address issues related to the use of modern techniques for formal specification and formal verification of robotic tasks and actions that co-ordinate the behaviours of a network of robots to achieve the objectives of a mission. In contrast with the current approaches, where the validation of the tasks is performed by simulation covering a limited number of possible scenarios, in this case the validation is done using rigorous mathematical analysis of all the possible states of execution. The utilisation of formally defined languages for the co-ordination of the behaviours will drastically reduce the specification, testing and debugging interval while it will highly improve our confidence on the up-loaded code.
1. INTRODUCTION
In the preparation of the ESA AURORA program, which targets the robotic and human exploration of the Solar system bodies holding promise for traces of life, Mars has been naturally designed as the first step before organising more ambitious enterprises.
On the basis of the technologies available in the next 20 or 30 years from now, by 2020-2030 an international human mission to Mars may be a reality. In this context, robotic missions will prepare the human missions, by:
- collecting as much scientific and engineering data as possible without human scientists in situ,
- constructing facilities for the crew, energy and material resources generation,
- maintaining the above-mentioned facilities,
- supporting in human exploration tasks which would be too risky, too complex, or too time-consuming,
- performing crew-independent exploration tasks under control of the humans on ground or on the planetary surface.
Analysis conducted by NASA and other space agencies as well and by an ESA internal ‘Group de reflection’, put in evidence that advanced Automation and Robotics are key mission enabling technologies for Mars exploration. In particular it has been concluded that a “robotic colony” on Mars would be of major strategic interest to Europe. These conclusions have been confirmed by the AROMA study ([1]) that provided also a reference A&R systems/technologies for a human Mars exploration programme.
Figure-1: AROMA Technology Inventory
Automation technologies can be grouped into two classes: telerobotics, which is the remote computer-assisted manipulation of equipment and materials, and systems autonomy, which includes intelligent automated control, monitoring and diagnosis. Autonomous machines are very probably the most suitable type for Mars surface applications. Autonomous behaviour based machines evolve in an entirely autonomous way, given the total absence of control of a
programming/supervisory link with an operator station.
In this scenario, an operator station plans and then refines the mission, generating a set of tasks to be interpreted and performed by the robot. The robot is fully autonomous at task level. It receives task assignments, which it transforms into sequences of actions using its own interpretation and planning capabilities. Tasks are therefore a temporal and logical composition of elementary actions able to achieve an objective in a context-dependant way, providing possibly predefined corrective actions to be launched in case of unsuccessful execution. Our work in the MUROCO project ([2]) focuses on actions and tasks formal modelling, specification and verification aspects.
- First, it consists to propose a framework for the specification of the tasks that allows the software engineer that prepares these tasks to perform, before launch, formal verification procedures and therefore to ensure that the programmed system will behave in conformity with its constraints.
- Second, we address verification issues, from a logical point of view. We put the stress on the systematisation of the verification procedure in the context of the robotics tasks and actions.
- Third, we consider the impact over the tasks specification and verification of the distributed aspect of a multi-robot system.
Actually, the realisation of a task request the co-ordination of actions possibly located on different robot controllers. We will examine the possibility to specify and verify the tasks in a single centralised program and afterwards to formally distribute it on the robot controllers in such a way that the parallel execution of the programs on each robot controller implements the initial one. This aspect is not further developed in this paper; we refer the reader to [2].
Konstantinos Kapellos, Daniele Galardini*
Frédéric Didot**
*TRASYS Space, Av. Ariane 7, B-1200 Brussels, Belgium
**ESA, ESTEC, Noordwijk, The Netherlans
No comments:
Post a Comment