Verification of a cruise control system using counterexample-guided search

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.