Task level specification and formal verification of robotics control systems: State of the art and case study
| Autor: | Dan Simon, M. Jourdant, Konstantinos Kapellos, Bernard Espiau |
|---|---|
| Rok vydání: | 1999 |
| Předmět: |
Functional verification
business.industry Computer science Robotics Control engineering Field (computer science) Computer Science Applications Theoretical Computer Science Control and Systems Engineering Logical conjunction Formal specification Robot Verification Artificial intelligence Software engineering business Formal verification |
| Zdroj: | International Journal of Systems Science. 30:1227-1245 |
| ISSN: | 1464-5319 0020-7721 |
| DOI: | 10.1080/002077299291697 |
| Popis: | 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 syste... |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|