×

Task level specification and formal verification of robotics control systems: State of the art and case study. (English) Zbl 1015.93534

Summary: This paper addresses the problem of specification and formal verification of complex applications in advanced robotics systems. In the first part, the need for such studies is presented, and the state of the art in the field is given, ranging from computer science to robotics. Then, the key features used in the paper are presented. They are called the robot task and the robot procedure respectively and allow us to specify in a structured way all the elements of robot controllers from the continuous and discrete time specification to implementation aspects. They are both integrated in the ORCCAD design environment. In the following, verification issues are described in depth, from the logical and temporal point of view. They are illustrated by a real example of automatic vehicle driving, in which various properties are proved and abstract views are built. The conclusion gives an evaluation of the obtained results, expresses some requirements and draws guidelines for the future. The interest of hybrid system models is particularly emphasized.

MSC:

93C85 Automated systems (robots, etc.) in control theory

Software:

Ptolemy; Coq; PVS
PDFBibTeX XMLCite
Full Text: DOI