2015年01月09日　　Friday Lunch Seminar
12:15 〜 13:00

CiNet　1F　Conference Room

“Analyzing the dynamics of concurrent systems thanks to model-checking based approaches.”

Morgan Magnin

Computer Science at Ecole Centrale de Nantes, France

Abstract:

Formal verification through model-checking has grown continuously over the past twenty years. Model-checking is based on the construction of a (discrete or timed) model describing the behavior of the system to analyze, the formalization of expected properties in a suitable logic and the use of efficient algorithms to check whether the model satisfies the aforementioned properties. First designed to help the automatic verification of embedded systems and software code, model-checking have recently seen its applications fields be multiplied, especially in the field of real-time systems, system engineering and systems biology.

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.

Our work focuses on the analysis of the dynamical behaviors of such complex systems. We design and adapt model-checking techniques to address such models, with a specific emphasis on biological regulatory networks. In order to address networks involving hundreds of components, we recently introduced a new framework, called Process Hitting. Establishing relationships between the components at the most atomic level possible, the Process Hitting opens the way to many static analysis and abstract interpretation methods to study complex dynamic properties.

In this talk, we will present our general approach to model concurrent systems, the Process Hitting modeling approach and the methods we designed to analyze its dynamics. We will illustrate its benefits and give some ideas of its applicability to different fields where concurrency is a key feature.

About CiNet’s Friday Lunch Seminars:
The Friday Lunch Seminar is CiNet’s main regular meeting series, held every week at 12:15 in the beautiful main lecture theatre on the ground floor at CiNet. The talks are typically 40mins long and orientated towards an inter-disciplinary audience. They are informal, social, and most people bring their own lunch to eat during the talk. They are open to anyone who is feeling curious and wants to come, regardless of where you work.