Model Checking of Hybrid Systems Using Shallow Synchronization - Formal Techniques for Distributed Systems Access content directly
Conference Papers Year : 2010

Model Checking of Hybrid Systems Using Shallow Synchronization


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.
Fichier principal
Vignette du fichier
61170153.pdf (178.56 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01055156 , version 1 (11-08-2014)





Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta. Model Checking of Hybrid Systems Using Shallow Synchronization. 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. pp.155-169, ⟨10.1007/978-3-642-13464-7_13⟩. ⟨hal-01055156⟩
94 View
241 Download



Gmail Facebook X LinkedIn More