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.
Document type :
Reports
Complete list of metadatas

Cited literature [70 references]  Display  Hide  Download

https://hal.inria.fr/inria-00073974
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:12:38 PM
Last modification on : Wednesday, April 11, 2018 - 1:53:44 AM
Long-term archiving on : Monday, April 5, 2010 - 12:02:59 AM

Identifiers

  • HAL Id : inria-00073974, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

243

Files downloads

292