Title :
Formal verification of hybrid systems using CheckMate: a case study
Author :
Silva, B. Izaias ; Krogh, Bruce H.
Author_Institution :
Dept. of Electr. & Comput. Eng., Carnegie Mellon Univ., Pittsburgh, PA, USA
Abstract :
We present a formal verification of a control algorithm from the literature for a four-cylinder four-stroke engine in the cutoff mode. The controlled system is modeled, simulated and verified using CheckMate, a tool for formal verification of hybrid systems developed at Carnegie Mellon University. CheckMate automatically constructs a polyhedral-invariant hybrid automaton (PIHA) from a Matlab/Simulink model of the hybrid system and performs the verification using discrete model approximations. This case study illustrates how verification can be performed directly on a model of the hybrid system dynamics without first constructing an approximation to the continuous dynamics using timed automata or linear hybrid automata models
Keywords :
automata theory; control system analysis computing; digital simulation; formal verification; internal combustion engines; mechanical engineering computing; CheckMate; Matlab/Simulink model; PIHA; cutoff mode; discrete model approximations; formal verification; four-cylinder four-stroke engine; hybrid system dynamics; polyhedral-invariant hybrid automaton; Automata; Automatic control; Automotive engineering; Computer aided software engineering; Computer languages; Engines; Formal verification; Graphical user interfaces; Mathematical model; Vehicle dynamics;
Conference_Titel :
American Control Conference, 2000. Proceedings of the 2000
Conference_Location :
Chicago, IL
Print_ISBN :
0-7803-5519-9
DOI :
10.1109/ACC.2000.879487
