Title :
Verifying switched-mode computer controlled systems
Author :
Kapinski, James ; Krogh, Bruce H.
Author_Institution :
Dept. of Electr. & Comput. Eng., Carnegie Mellon Univ., Pittsburgh, PA, USA
Abstract :
This paper presents a new approach to verifying properties of computer control systems with periodic sampling when the control programs include both continuous-variable computations and discrete-state transitions (mode switching). We focus on the novel aspects of the approach, which are (1) a formal model for hybrid systems with continuous-time and discrete-time behavior and (2) a method for computing conservative approximations to the sets of reachable states. The formal model and computational routines are incorporated into CheckMate, a MATLAB-based tool for verification of properties of hybrid dynamic systems. This tool is being applied to the verification of embedded controllers in automotive engines.
Keywords :
computerised control; formal verification; internal combustion engines; reachability analysis; road vehicles; sampled data systems; CheckMate; MATLAB-based tool; automotive engines; conservative approximations; continuous-time behavior; continuous-variable computations; discrete-state transitions; discrete-time behavior; embedded controller verification; formal model; hybrid dynamic systems; mode switching; periodic sampling; reachable states; sampled-data computer controlled system; switched-mode computer controlled system verification; variable cam timing system; Automata; Automatic control; Automotive engineering; Computational modeling; Computer languages; Control systems; Engines; Mathematical model; Sampling methods; Vehicle dynamics;
Conference_Titel :
Computer Aided Control System Design, 2002. Proceedings. 2002 IEEE International Symposium on
Print_ISBN :
0-7803-7388-X
DOI :
10.1109/CACSD.2002.1036936
