Souha Ben Rayana
4 November 2016 - 14h00
Compositional Verification of Component-Based Real-time Systems and Applications. (Phd Defense)
by Souha Ben Rayana from Verimag, Grenoble Alpes University
Abstract: Compositional Verification aims at breaking down the complexity of the verification task by relying on the separate analysis of the sub-components and inferring global properties of the system from their local properties. In the framework of real-time systems, one main obstacle for developing fully compositional methods is the synchronous model of time.
We propose a verification method based on the deductive approach where the set of the reachable states of the system is over-approximated by an invariant computed in a fully compositional manner. It comprises local component invariants and an interaction invariant characterizing the interactions between the components.
In addition, we introduce auxiliary clocks, called history clocks, which allow to automatically generate new invariants capturing the constraints induced by the time-synchronizations between the different components. We completed this compositional invariant generation approach with a counterexample-based invariant enforcement module analyzing iteratively the generated counterexamples.
Besides its scalability, the method can be extended to the uniform verification of parameterized timed systems.
The compositional verification method was implemented in the RTD-Finder tool.
The experimental results show that the verification time for large systems is drastically reduced in comparison with exploration techniques, especially when the global invariant catches the safety property of interest.
Jury:
Prof. Ahmed Bouajjani
Université Paris Diderot, Rapporteur
Prof. Kim Guldstrand Larsen
Université D’Aalborg , Rapporteur
Prof. Erika Ábrahám
Université de RWTH Aachen , Examinateur
Prof. Florence Maraninchi
Université Grenoble Alpes et INP Grenoble , Examinateur
Prof. Doron Peled
Université de Bar Ilan, Examinateur
Dr. Natarajan Shankar SRI International, Examinateur
Prof. Saddek Bensalem,
Université Grenoble Alpes, Directeur de thèse
Dr. Marius Bozga
Ingénieur de recherche - HDR, CNRS, Co-Directeur de thèse
