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

    72 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
    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

    Conference

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

    Fingerprint

    Hybrid systems
    Model checking
    Dynamical systems
    Systems analysis

    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 ; Krogh, Bruce H. ; Stursberg, Olaf ; Theobald, Michael. / 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",

    }

    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; Krogh, Bruce H.; Stursberg, Olaf; Theobald, Michael.

    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 proceedingConference contributionAcademicpeer-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

    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

    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). https://doi.org/10.1007/3-540-36577-X_14