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.
|Number of pages||18|
|Journal||International Journal of Foundations of Computer Science|
|Publication status||Published - Aug 2006|