Inductive verification of hybrid automata with strongest postcondition calculus

Daisuke Ishii, Guillaume Melquiond, Shin Nakajima

    研究成果: Conference contribution

    1 被引用数 (Scopus)

    抄録

    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.

    本文言語English
    ホスト出版物のタイトルLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    ページ139-153
    ページ数15
    7940 LNCS
    DOI
    出版ステータスPublished - 2013
    イベント10th International Conference on Integrated Formal Methods, IFM 2013 - Turku
    継続期間: 2013 6 102013 6 14

    出版物シリーズ

    名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    7940 LNCS
    ISSN(印刷版)03029743
    ISSN(電子版)16113349

    Other

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

    ASJC Scopus subject areas

    • コンピュータ サイエンス(全般)
    • 理論的コンピュータサイエンス

    フィンガープリント

    「Inductive verification of hybrid automata with strongest postcondition calculus」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

    引用スタイル