On the Validation of Robotics Control Systems Part I: High Level Specification and Formal Verification

Bernard Espiau 1 Konstantin Kapellos 2 Muriel Jourdan 1 Daniel Simon 2
1 BIP - Biped Robot
Inria Grenoble - Rhône-Alpes
2 ICARE - Instrumentation, control and architecture of advanced robots
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This report presents an extensive work on the specification and the formal verification of complex applications in advanced robotics systems. In a first part, the need for such studies is presented, and a state-of-the-art in the field is given, evolving from the computer science area to the robotics one. Then, the key features used in the paper are presented. They are called the Robot Task and the Robot Procedure respectively, and are both integrated in the {\sc ORCCAD} design environment. In the following, verification issues are described in depth, from the logical point of view as well as from the temporal one. They are illustrated by real examples, in which various properties are proved and abstract views are built. The conclusion gives an evaluation of the obtained results, expresses some requirements and draw guidelines for the future. The interest of hybrid systems is particularly emphasized.
Type de document :
[Research Report] RR-2719, INRIA. 1995
Liste complète des métadonnées

Littérature citée [70 références]  Voir  Masquer  Télécharger

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:12:38
Dernière modification le : mercredi 11 avril 2018 - 01:53:44
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:02:59



  • HAL Id : inria-00073974, version 1



Bernard Espiau, Konstantin Kapellos, Muriel Jourdan, Daniel Simon. On the Validation of Robotics Control Systems Part I: High Level Specification and Formal Verification. [Research Report] RR-2719, INRIA. 1995. 〈inria-00073974〉



Consultations de la notice


Téléchargements de fichiers