An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems.
Wednesday 8 December 2010 at 14:30 in Cachan.
Salle de Conférences, Pavillon des Jardins,
École Normale Supérieure de Cachan.
See the access plan to the campus, and the plan of the campus (pavillon des jardins is building number 5).
| Eugene Asarin | President |
| Bernard Berthomieu | Reviewer |
| Franck Cassez | Reviewer |
| Emmanuelle Encrenaz-Tiphene | Advisor |
| Laurent Fribourg | Advisor |
| Marta Kwiatkowska | Examiner |
| Kim G. Larsen | Examiner |
This thesis proposes a novel approach for the synthesis of delays for timed systems. When verifying a real-time system, e.g., a hardware device or a communication protocol, it is important to check that not only the functional but also the timed behavior is correct. This correctness depends on the values of the delays of internal operations and of the environment.
Formal verification methods guarantee the correctness of a timed system for a given set of delays, but do not give information for other values of the delays. Checking the correctness of for various values of those delays can be difficult and time consuming. It is thus interesting to consider that these delays are parameters. The problem then consists in synthesizing "good values" for those parameters, i.e., values for which the system is guaranteed to behave well.
We are here interested in the synthesis of parameters in the framework of timed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same time-abstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points of a bounded parameter domain, we are then able to partition the parametric space into good and bad zones, with respect to a given property one wants to verify. This gives a behavioral cartography of the system.
This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols.
Keywords: verification, model checking, timed systems, parametric timed automata, synthesis of parameters, hardware verification, probabilistic timed automata, randomized protocols.
The final version of my thesis can be found here.
The slides of my defense are available here.
See also: