salle A. Turing CE4
23 January 2014 - 14h00
Compositional Verification of Component- Based Real-time Systems and Applications
by Souha Ben Rayana from Verimag
Abstract: The aim of this thesis is to overcome the state-space explosion problem related to the verification of timed systems with great number of components. Some methods for compositional verification where proposed for untimed systems. However, for timed systems, another important issue is encountered. In fact, the main difficulty with compositional verification of timed system is that calculating the local invariant of one component requires the desynchronization from other components. In the other side, time synchronization between components should be further considered in the calculation of the global property of the system.
To this end, we make use of auxiliary clocks, which we call « history clocks », to automatically generate new invariants. History clocks are intended to capture the constraints induced by the synchronizations between components. This idea allows a pure compositional method for the calculation of global invariants of real-time systems.
The method has been implemented in a prototype and was successfully experimented on several case studies.
Now, it is being implemented as an extension of the D-Finder tool [1].
1. S. Bensalem, M. Bozga, J. Sifakis, and T.-H. Nguyen. Compositional verification ?for component-based systems and application. In Proceedings of ATVA, 2008.
