Title :
Using model checking to guarantee safety in automatically-synthesized real-time controllers
Author :
Musliner, David J. ; Goldman, Robert P. ; Pelican, Michael J.
Author_Institution :
Autom. Reasoning Group, Honeywell Technol. Center, Minneapolis, MN, USA
Abstract :
Concerns the development of autonomous, flexible control systems for mission-critical applications such as unmanned aerial vehicles (UAV) and deep space probes. These applications require hybrid real-time control systems, capable of effectively managing both discrete and continuous controllable parameters to maintain system safety and achieve system goals. Using the CIRCA architecture and its state space planner (SSP) for adaptive real-time control systems, these controllers are synthesized automatically and dynamically, online, while the platform is operating. Unlike many other AI planning systems, CIRCA´s automatically-generated control plans have strong temporal semantics and provide safety guarantees, ensuring that the controlled system will avoid all forms of mission-critical failure. This paper is intended to convey an intuitive, qualitative understanding of the way CIRCA verifies its plans using model checking techniques
Keywords :
adaptive control; aerospace robotics; control system CAD; mobile robots; real-time systems; robot programming; safety; state-space methods; temporal logic; CIRCA architecture; SSP; UAV; adaptive real-time control systems; automatically-synthesized real-time controllers; autonomous flexible control systems; deep Space probes; hybrid real-time control systems; mission-critical applications; mission-critical failure avoidance; model checking; safety; state space planner; temporal semantics; unmanned aerial vehicles; Automatic control; Control system synthesis; Control systems; Mission critical systems; Probes; Real time systems; Safety; Space missions; State-space methods; Unmanned aerial vehicles;
Conference_Titel :
Robotics and Automation, 2000. Proceedings. ICRA '00. IEEE International Conference on
Conference_Location :
San Francisco, CA
Print_ISBN :
0-7803-5886-4
DOI :
10.1109/ROBOT.2000.844045