Verification of a cruise control system using counterexample-guided search

Olaf Stursberg*, Ansgar Fehnker, Zhi Han, Bruce H. Krogh

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

41 Citations (Scopus)


Formal verification has been identified by the research community as a useful step in logic controller design since it reveals algorithmically whether the controller in conjunction with the controlled plant satisfies given design specifications. If it is necessary, however, to model the continuous/hybrid behavior of the plant, the verification is a computationally expensive task. This paper shows for the example of a cruise control system that the recently proposed approach of counterexample-guided verification can reduce the computational costs considerably. The method generates a sequence of abstractions, for which those behaviors (the counterexamples) are identified that potentially violate the specifications. The paper presents a tailor-made sequence of validation methods that aim at checking the existence of these behaviors for the hybrid model of the controlled plant with as small computational costs as possible.

Original languageEnglish
Pages (from-to)1269-1278
Number of pages10
JournalControl engineering practice
Issue number10
Publication statusPublished - Oct 2004
Externally publishedYes


  • Abstraction
  • Automata
  • Counterexample
  • Hybrid systems
  • Model refinement
  • Reachability analysis
  • Verification


Dive into the research topics of 'Verification of a cruise control system using counterexample-guided search'. Together they form a unique fingerprint.

Cite this