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

    ASJC Scopus subject areas

    • Computer Science(all)
    • Theoretical Computer Science

    Fingerprint Dive into the research topics of 'Inductive verification of hybrid automata with strongest postcondition calculus'. Together they form a unique fingerprint.

    Cite this