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)

Abstract

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
Volume12
Issue number10
DOIs
Publication statusPublished - Oct 2004
Externally publishedYes

Keywords

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

Fingerprint

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

Cite this