Model Checking of Hybrid Systems Using Shallow Synchronization

Abstract : Hybrid automata are a widely accepted modeling framework for systems with discrete and continuous variables. The traditional semantics of a network of automata is based on interleaving, and requires the construction of a monolithic hybrid automaton based on the composition of the automata. This destroys the structure of the network and results in a loss of efficiency, especially using bounded model checking techniques. An alternative compositional semantics, called "shallow synchronization", exploits the locality of transitions and relaxes time synchronization. The semantics is obtained by composing traces of the local automata, and superimposing compatibility constraints resulting from synchronization. In this paper, we investigate the different symbolic encodings of the reachability problem of a network of hybrid automata. We propose a novel encoding based on the shallow synchronization semantics, which allows different strategies for searching local paths that can be synchronized. We implemented a bounded reachability search based on the use of an incremental Satisfiability-Modulo-Theory solver. The experimental results confirm that the new encoding often performs better than the one based on interleaving.
Type de document :
Communication dans un congrès
John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.155-169, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_13〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01055156
Contributeur : Hal Ifip <>
Soumis le : lundi 11 août 2014 - 16:32:25
Dernière modification le : vendredi 11 août 2017 - 16:16:35
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:15:49

Fichier

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

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta. Model Checking of Hybrid Systems Using Shallow Synchronization. John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.155-169, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_13〉. 〈hal-01055156〉

Partager

Métriques

Consultations de la notice

230

Téléchargements de fichiers

83