Model-Based Verification for Automatic Synthesis of Real-Time Controllers

Robert P. Goldman, David J. Musliner, and Michael J. S. Pelican

We have developed a novel technique for automatically synthesizing hard real-time reactive controllers using model-checking verification. Our algorithm builds a controller incrementally, using a timed automaton model to check each partial controller for correctness. The verification model captures both the controller design and the semantics of its execution environment. If the controller is found to be incorrect, information from the verification system is used to direct the search for improvements. This paper describes how our controller synthesis process uses verification, and explains in detail how we model the execution of the real time subsystem of the CIRCA intelligent control architecture.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.