Formal methods for the inference of discrete and timing parameters in large-scale dynamic systems
Speaker: Morgan Magnin, École Centrale de Nantes
Date: May 9th, 2013
Place: room 102, Faculty of Science Bldg. 7, Hongo Campus, The University of Tokyo
Formal verification through model-checking have grown continuously over the past twenty years. While model-checking first targeted discrete-event systems, it has appeared that some critical applications (for example, those involving task scheduling issues) require taking into account the quantitative time between transitions and/or some actions. To achieve this, logical time — usually captured by models like finite automata or Petri nets — is no longer sufficient. That is why a wide range of research studies have emerged in the field of timed systems for more than 20 years.
When modeling a timed system, the question of choosing an appropriate time semantics — among dense-time and discrete-time — is crucial. In the first approach, time is considered as a dense quantity (i.e. the state of the system can change at any moment) and, in the second one, as a discrete variable (time progress is ensured by clock ticks and the global system may evolve only at these peculiar time steps). During the first part of the talk, we will examine the respective merits of dense-time and discrete-time semantics, especially in the case of timed extensions of Petri nets. We will discuss the impact of these results on the model-checking of formal properties expressed through modal logics. We will illustrate the merits of our approach on an example coming from biological systems, in a context of inference of timing parameters.
Discussing the limits of such a methodology (especially in the case of large-scale systems), we will then justify the recent introduction of a new formalism, named the Process Hitting, to model concurrent systems having components with a few qualitative levels. Thanks to the particular structure of interactions within a Process Hitting, very efficient static analysis methods have been developed to tackle the formal analysis of systems with hundreds of components. We will focus on the key ideas behind this formalism and the related algorithms. We will illustrate the merits of constraint programming (especially Answer Set Programming) applied to this framework, in a context of automatic inference of models. Finally, we will give a taste of how future extensions, incorporating timing information, could allow to infer quantitative timing information about the evolution of real-life systems.