Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus

Daisuke Ishii 1 Guillaume Melquiond 2, 3 Shin Nakajima 1
1 NII - National Institute of Informatics [Tokyo]
2 LRI - Laboratoire de Recherche en Informatique
3 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Keywords : strongest postconditions invariant generation hybrid systems safety analysis Hoare logic
Type de document :
Communication dans un congrès
Einar Broch Johnsen and Luigia Petre. iFM - 10th International Conference on Integrated Formal Methods - 2013, Jun 2013, Turku, Finland. Springer, 7940, pp.139-153, 2013, <10.1007/978-3-642-38613-8_10>
Liste complète des métadonnées

https://hal.inria.fr/hal-00806701
Contributeur : Guillaume Melquiond <>
Soumis le : mardi 2 avril 2013 - 11:08:51
Dernière modification le : jeudi 9 février 2017 - 16:00:21
Document(s) archivé(s) le : mercredi 3 juillet 2013 - 04:04:51

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UMR8623 | INSMI | LRI-VALS | TDS-MACS | CENTRALESUPELEC

Citation

Daisuke Ishii, Guillaume Melquiond, Shin Nakajima. Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. Einar Broch Johnsen and Luigia Petre. iFM - 10th International Conference on Integrated Formal Methods - 2013, Jun 2013, Turku, Finland. Springer, 7940, pp.139-153, 2013, <10.1007/978-3-642-38613-8_10>. <hal-00806701>

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de
la notice

433

Téléchargements du document

160

Contact


archive-ouverte@inria.fr