Specifying and Verifying Robotic Tasks

This paper presents an approach to the specification of requirements, and verification of design, for a robot or other intelligent system. Formal mathematical reasoning is used to show that a design conforms to the system requirements. Typically the requirements define safety and functionality constraints on the system and components. Formal analysis allows the system designer to evaluate the system behavior and verify the system parameters in order to guarantee safe and robust system performance. The approach is demonstrated on a typical robotic task -- visual grasping. 1 Introduction The growing number of computer-controlled systems presents a major challenge: development of reliable, robust, and safe real-time intelligent systems. Robots and electro-mechanical systems (such as many consumer products) are capable of adjusting their behavior to a wide variety of circumstances. These systems are based on a combination of different structures ranging from low-level feedback loops to hi..