Formal verification of hybrid systems using CheckMate: a case study

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. C...

Full description

Saved in:
Bibliographic Details
Main Authors: Silva, B.I., Krogh, B.H.
Format: Conference Proceeding
Language:English
Subjects:
Automata
Automatic control
Automotive engineering
Computer aided software engineering
Computer languages
Engines
Formal verification
Graphical user interfaces
Mathematical model
Vehicle dynamics
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0743-1619
2378-5861
DOI:10.1109/ACC.2000.879487