Inductive verification of hybrid automata with strongest postcondition calculus

Daisuke Ishii, Guillaume Melquiond, Shin Nakajima

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    1 Citation (Scopus)

    Abstract

    Safety verification of hybrid systems is a key technique in developing embedded systems that have a strong coupling with the physical environment. We propose an automated logical analytic method for verifying a class of hybrid automata. The problems are more general than those solved by the existing model checkers: our method can verify models with symbolic parameters and nonlinear equations as well. First, we encode the execution trace of a hybrid automaton as an imperative program. Its safety property is then translated into proof obligations by strongest postcondition calculus. Finally, these logic formulas are discharged by state-of-the-art arithmetic solvers (e.g., Mathematica). Our proposed algorithm efficiently performs inductive reasoning by unrolling the execution for some steps and generating loop invariants from verification failures. Our experimental results along with examples taken from the literature show that the proposed approach is feasible.

    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Pages139-153
    Number of pages15
    Volume7940 LNCS
    DOIs
    Publication statusPublished - 2013
    Event10th International Conference on Integrated Formal Methods, IFM 2013 - Turku
    Duration: 2013 Jun 102013 Jun 14

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume7940 LNCS
    ISSN (Print)03029743
    ISSN (Electronic)16113349

    Other

    Other10th International Conference on Integrated Formal Methods, IFM 2013
    CityTurku
    Period13/6/1013/6/14

    Fingerprint

    Hybrid Automata
    Calculus
    Safety
    Mathematica
    Strong Coupling
    Hybrid systems
    Hybrid Systems
    Nonlinear equations
    Embedded systems
    Embedded Systems
    Nonlinear Equations
    Reasoning
    Trace
    Logic
    Verify
    Invariant
    Experimental Results
    Model
    Class

    ASJC Scopus subject areas

    • Computer Science(all)
    • Theoretical Computer Science

    Cite this

    Ishii, D., Melquiond, G., & Nakajima, S. (2013). Inductive verification of hybrid automata with strongest postcondition calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7940 LNCS, pp. 139-153). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7940 LNCS). https://doi.org/10.1007/978-3-642-38613-8_10

    Inductive verification of hybrid automata with strongest postcondition calculus. / Ishii, Daisuke; Melquiond, Guillaume; Nakajima, Shin.

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7940 LNCS 2013. p. 139-153 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7940 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Ishii, D, Melquiond, G & Nakajima, S 2013, Inductive verification of hybrid automata with strongest postcondition calculus. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 7940 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7940 LNCS, pp. 139-153, 10th International Conference on Integrated Formal Methods, IFM 2013, Turku, 13/6/10. https://doi.org/10.1007/978-3-642-38613-8_10
    Ishii D, Melquiond G, Nakajima S. Inductive verification of hybrid automata with strongest postcondition calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7940 LNCS. 2013. p. 139-153. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-38613-8_10
    Ishii, Daisuke ; Melquiond, Guillaume ; Nakajima, Shin. / Inductive verification of hybrid automata with strongest postcondition calculus. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7940 LNCS 2013. pp. 139-153 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    @inproceedings{5702846bc0904eb3abe0e5bbf8208106,
    title = "Inductive verification of hybrid automata with strongest postcondition calculus",
    abstract = "Safety verification of hybrid systems is a key technique in developing embedded systems that have a strong coupling with the physical environment. We propose an automated logical analytic method for verifying a class of hybrid automata. The problems are more general than those solved by the existing model checkers: our method can verify models with symbolic parameters and nonlinear equations as well. First, we encode the execution trace of a hybrid automaton as an imperative program. Its safety property is then translated into proof obligations by strongest postcondition calculus. Finally, these logic formulas are discharged by state-of-the-art arithmetic solvers (e.g., Mathematica). Our proposed algorithm efficiently performs inductive reasoning by unrolling the execution for some steps and generating loop invariants from verification failures. Our experimental results along with examples taken from the literature show that the proposed approach is feasible.",
    author = "Daisuke Ishii and Guillaume Melquiond and Shin Nakajima",
    year = "2013",
    doi = "10.1007/978-3-642-38613-8_10",
    language = "English",
    isbn = "9783642386121",
    volume = "7940 LNCS",
    series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
    pages = "139--153",
    booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

    }

    TY - GEN

    T1 - Inductive verification of hybrid automata with strongest postcondition calculus

    AU - Ishii, Daisuke

    AU - Melquiond, Guillaume

    AU - Nakajima, Shin

    PY - 2013

    Y1 - 2013

    N2 - Safety verification of hybrid systems is a key technique in developing embedded systems that have a strong coupling with the physical environment. We propose an automated logical analytic method for verifying a class of hybrid automata. The problems are more general than those solved by the existing model checkers: our method can verify models with symbolic parameters and nonlinear equations as well. First, we encode the execution trace of a hybrid automaton as an imperative program. Its safety property is then translated into proof obligations by strongest postcondition calculus. Finally, these logic formulas are discharged by state-of-the-art arithmetic solvers (e.g., Mathematica). Our proposed algorithm efficiently performs inductive reasoning by unrolling the execution for some steps and generating loop invariants from verification failures. Our experimental results along with examples taken from the literature show that the proposed approach is feasible.

    AB - Safety verification of hybrid systems is a key technique in developing embedded systems that have a strong coupling with the physical environment. We propose an automated logical analytic method for verifying a class of hybrid automata. The problems are more general than those solved by the existing model checkers: our method can verify models with symbolic parameters and nonlinear equations as well. First, we encode the execution trace of a hybrid automaton as an imperative program. Its safety property is then translated into proof obligations by strongest postcondition calculus. Finally, these logic formulas are discharged by state-of-the-art arithmetic solvers (e.g., Mathematica). Our proposed algorithm efficiently performs inductive reasoning by unrolling the execution for some steps and generating loop invariants from verification failures. Our experimental results along with examples taken from the literature show that the proposed approach is feasible.

    UR - http://www.scopus.com/inward/record.url?scp=84886022235&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=84886022235&partnerID=8YFLogxK

    U2 - 10.1007/978-3-642-38613-8_10

    DO - 10.1007/978-3-642-38613-8_10

    M3 - Conference contribution

    SN - 9783642386121

    VL - 7940 LNCS

    T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    SP - 139

    EP - 153

    BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    ER -