Verification of hybrid systems based on counterexample-guided abstraction refinement

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

doi:10.1007/3-540-36577-X_14

Verification of hybrid systems based on counterexample-guided abstraction refinement

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

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

86 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
Place of Publication	Berlin
Publisher	Springer, Springer Nature
Pages	192-207
Number of pages	16
ISBN (Print)	9783540008989, 3540008985
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, TACAS 2003: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 - Warsaw, Poland Duration: 7 Apr 2003 → 11 Apr 2003

Publication series

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

Conference

Conference	9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003
Abbreviated title	TACAS 2003
Country/Territory	Poland
City	Warsaw
Period	7/04/03 → 11/04/03

Access to Document

10.1007/3-540-36577-X_14

Cite this

Clarke, E., Fehnker, A., Han, Z., Krogh, B., 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, Springer Nature. https://doi.org/10.1007/3-540-36577-X_14

Clarke, Edmund ; 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. Berlin : Springer, Springer Nature, 2003. pp. 192-207 (Lecture Notes in Computer Science).

@inproceedings{92594d97c4fb4678a27a36cc75595002,

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 = "Edmund Clarke and Ansgar Fehnker and Zhi Han and Bruce Krogh and Olaf Stursberg and Michael Theobald",

year = "2003",

doi = "10.1007/3-540-36577-X\_14",

language = "English",

isbn = "9783540008989",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "192--207",

editor = "Hubert Garavel and John Hatcliff",

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

address = "United States",

note = "9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003 : Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, TACAS 2003 ; Conference date: 07-04-2003 Through 11-04-2003",

}

Clarke, E, Fehnker, A, Han, Z, Krogh, B, 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, Springer Nature, Berlin, pp. 192-207, 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 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; 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. Berlin: Springer, Springer Nature, 2003. p. 192-207 (Lecture Notes in Computer Science; Vol. 2619).

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

TY - GEN

T1 - Verification of hybrid systems based on counterexample-guided abstraction refinement

AU - Clarke, Edmund

AU - Fehnker, Ansgar

AU - Han, Zhi

AU - Krogh, Bruce

AU - Stursberg, Olaf

AU - Theobald, Michael

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.

UR - https://www.scopus.com/pages/publications/35248899265

U2 - 10.1007/3-540-36577-X_14

DO - 10.1007/3-540-36577-X_14

M3 - Conference proceeding contribution

SN - 9783540008989

SN - 3540008985

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, Springer Nature

CY - Berlin

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

Y2 - 7 April 2003 through 11 April 2003

ER -

Clarke E, Fehnker A, Han Z, Krogh B, 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. Berlin: Springer, Springer Nature. 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

Other files and links

Fingerprint

Cite this