virtual seminar
11 December 2020 - 10h30
Compositional Generation of Invariants for Timed Systems
by Marius Bozga from VERIMAG
Abstract: zoom link
https://univ-grenoble-alpes-fr.zoom.us/j/99529870648?pwd=b04vSUpyRmJDL2k3OUZxWHRSc3R0dz09
Meeting ID: 995 2987 0648
Passcode: 932215
(Note that this seminar was previously announced for Friday Dec 4. It is now rescheduled for Friday Dec 11)
This presentation recalls our compositional method developed to address the state space explosion inherent in verification of timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints induced by the synchronisations between components. The method has been implemented in the RTD-Finder tool, successfully experimented on several benchmarks and extended to some restricted classes of parameterized and/or hybrid systems.
