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

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.