Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement

Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

81 Citations (Scopus)

Abstract

Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of infinite-state systems, in particular of hybrid systems. Following an approach originally developed for finite-state systems [1],[2], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space.We showhowsuch reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. A detailed example illustrates our counterexample-guided refinement procedure. Experimental results for a prototype implementation of the procedure indicate its advantages over existing methods.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings
EditorsHubert Garavel, John Hatcliff
PublisherSpringer
Pages192-207
Number of pages16
ISBN (Electronic)978-3-540-36577-8
ISBN (Print)978-3-540-00898-9
DOIs
Publication statusPublished - 2003
Externally publishedYes
Event9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003 - Warsaw, Poland
Duration: 7 Apr 200311 Apr 2003
Conference number: 9
http://vasy.inria.fr/tacas03/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2619
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003
Abbreviated titleTACAS 2003
Country/TerritoryPoland
CityWarsaw
Period7/04/0311/04/03
Internet address

Fingerprint

Dive into the research topics of 'Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement'. Together they form a unique fingerprint.

Cite this