Formal Modeling and Analysis of Timed Systems

Many applications, such as communication protocols, require models which integrate both real-time constraints, and randomization. The verification of such models is a challenging task since they combine dense-time and probabilities. To verify stochastic real-time systems, we propose a framework to perform the analysis of general stochastic transition systems (STSs). This methodology relies on two pillars: a decisiveness and abstraction. Decisiveness was introduced for denumerable Markov chains [1], and roughly speaking, it allows one to lift most analysis techniques from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. We explain how to generalize this central notion to dense-time stochastic models. In order to exploit decisiveness, we define a notion of abstraction, and we give general transfer properties from the abstract model to the concrete one. These are central to come up with qualitative and quantitative verification algorithms for STS. Our methodology applies for instance to stochastic timed automata (STA) and generalized semi-Markov processes (GSMP), two existing models combining dense-time and probabilities. This allows us on the one hand to recover existing results from the literature on these two models –with less effort and a unified view– and on the other hand to derive new approximation algorithms for STA and GSMP. The interested reader can refer to a joint article with Patricia Bouyer, Thomas Brihaye and Pierre Carlier for further details [2]. Short biography Nathalie Bertrand obtained her PhD from ENS Cachan in 2006, supervised by Philippe Schnoebelen. She spent a year at TU Dresden working with Christel Baier, and was in 2007 hired junior research scientist at Inria Rennes. Her expertise is in model checking specifically for probabilistic systems.