Hybrid system verification is not a sinecure the electronic throttle control case study

Abstract

Though model checking itself is a fully automated process, verifying correctness of a hybrid system design using model checking is not. This paper describes the necessary steps, and choices to be made, to go from an informal description of the problem to the final verification result for a formal model and requirement. It uses an automotive control system for illustration. © Springer-Verlag 2004.