Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement

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

doi:10.1007/3-540-36577-X_14

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 proceeding › Conference contribution › Academic › peer-review

85 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 language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	9th 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
Editors	Hubert Garavel, John Hatcliff
Publisher	Springer
Pages	192-207
Number of pages	16
ISBN (Electronic)	978-3-540-36577-8
ISBN (Print)	978-3-540-00898-9
DOIs	https://doi.org/10.1007/3-540-36577-X_14
Publication status	Published - 2003
Externally published	Yes
Event	9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003 - Warsaw, Poland Duration: 7 Apr 2003 → 11 Apr 2003 Conference number: 9 http://vasy.inria.fr/tacas03/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2619
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003
Abbreviated title	TACAS 2003
Country/Territory	Poland
City	Warsaw
Period	7/04/03 → 11/04/03
Internet address	http://vasy.inria.fr/tacas03/

Access to Document

10.1007/3-540-36577-X_14

Cite this

Clarke, E. M., Fehnker, A., Han, Z., Krogh, B. H., Stursberg, O., & Theobald, M. (2003). Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. In H. Garavel, & J. Hatcliff (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 9th 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 (pp. 192-207). (Lecture Notes in Computer Science; Vol. 2619). Springer. https://doi.org/10.1007/3-540-36577-X_14

Clarke, Edmund M. ; Fehnker, Ansgar ; Han, Zhi et al. / Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. Tools and Algorithms for the Construction and Analysis of Systems: 9th 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. editor / Hubert Garavel ; John Hatcliff. Springer, 2003. pp. 192-207 (Lecture Notes in Computer Science).

@inproceedings{a235fcc528a346efa348327909797c7e,

title = "Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement",

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.",

author = "Clarke, {Edmund M.} and Ansgar Fehnker and Zhi Han and Krogh, {Bruce H.} and Olaf Stursberg and Michael Theobald",

year = "2003",

doi = "10.1007/3-540-36577-X_14",

language = "English",

isbn = "978-3-540-00898-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "192--207",

editor = "Hubert Garavel and John Hatcliff",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003, TACAS 2003 ; Conference date: 07-04-2003 Through 11-04-2003",

url = "http://vasy.inria.fr/tacas03/",

}

Clarke, EM, Fehnker, A, Han, Z, Krogh, BH, Stursberg, O & Theobald, M 2003, Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. in H Garavel & J Hatcliff (eds), Tools and Algorithms for the Construction and Analysis of Systems: 9th 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. Lecture Notes in Computer Science, vol. 2619, Springer, pp. 192-207, 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003, Warsaw, Poland, 7/04/03. https://doi.org/10.1007/3-540-36577-X_14

Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. / Clarke, Edmund M.; Fehnker, Ansgar; Han, Zhi et al.
Tools and Algorithms for the Construction and Analysis of Systems: 9th 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. ed. / Hubert Garavel; John Hatcliff. Springer, 2003. p. 192-207 (Lecture Notes in Computer Science; Vol. 2619).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement

AU - Clarke, Edmund M.

AU - Fehnker, Ansgar

AU - Han, Zhi

AU - Krogh, Bruce H.

AU - Stursberg, Olaf

AU - Theobald, Michael

N1 - Conference code: 9

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-36577-X_14

DO - 10.1007/3-540-36577-X_14

M3 - Conference contribution

SN - 978-3-540-00898-9

T3 - Lecture Notes in Computer Science

SP - 192

EP - 207

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Garavel, Hubert

A2 - Hatcliff, John

PB - Springer

T2 - 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003

Y2 - 7 April 2003 through 11 April 2003

ER -

Clarke EM, Fehnker A, Han Z, Krogh BH, Stursberg O, Theobald M. Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. In Garavel H, Hatcliff J, editors, Tools and Algorithms for the Construction and Analysis of Systems: 9th 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. Springer. 2003. p. 192-207. (Lecture Notes in Computer Science). doi: 10.1007/3-540-36577-X_14

Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this