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
2 ICARE - Instrumentation, control and architecture of advanced robots

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.

Mots clés: ROBOTICS; CONTROL; FORMAL VERIFICATION

Domaines: Autre [cs.OH]

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⟩