Soutenance de thèse de Jan Stoecker

Jan Stoecker soutiendra le 10 décembre 2009 à 15h
au Grand Amphithéâtre de l'INRIA Grenoble Rhône-Alpes
655, avenue de l'Europe 38330 Montbonnot Saint Martin
(informations d'accès)

une thèse de doctorat de Grenoble INP (Institut National Polytechnique),
spécialité : informatique, intitulée :

"Un modèle intermédiaire pour la vérification des systèmes asynchrones embarqués temps réel : définition et application du langage ATLANTIF"

Thèse préparée dans le Centre de Recherche INRIA Grenoble Rhône-Alpes (équipe-projet Vasy),
sous la direction de M. Hubert GARAVEL et de M. Frédéric LANG.

COMPOSITION DU JURY :

• M. Roland GROZ, professeur à Grenoble INP (président du jury)
  
• M. Elie NAJM, professeur à Télécom ParisTech (rapporteur)
  
• M. François VERNADAT, professeur à l'INSA de Toulouse (rapporteur)
  
• M. Alain GRIFFAULT, maître de conférences à l'université de Bordeaux (examinateur)
  
• M. Hubert GARAVEL, directeur de recherche à l'INRIA Grenoble Rhône-Alpes (directeur de thèse)
  
• M. Frédéric LANG, chargé de recherche à l'INRIA Grenoble Rhône-Alpes (directeur de thèse)
  

La soutenance sera naturellement suivie d'un pot, à côté de l'amphithéâtre, auquel vous êtes tous cordialement invités.

Manuscrit (290 pages)

PDF

PS

Transparents de la soutenance

PDF

RESUME :

La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément.

Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple Uppaal) et les réseaux de Petri temporisés (par exemple Tina).

Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non-temporisés qui manipulent des données complexes.

Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur.

Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec Uppaal) et vers des réseaux de Petri temporisés (pour la vérification avec Tina). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple.

MOTS-CLES :

algèbre de processus, automate, concurrence, méthode formelle, modèle intermédiaire, temps-réel, réseau de Petri, vérification

TITLE:

An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language

ABSTRACT:

The validation of real-life critical systems raises the challenge of being able to formally model and verify complex data, asynchronous concurrency, and real-time aspects simultaneously.

High-level languages, such as those inheriting from the theoretical foundations of process algebras, provide a concise syntax and a high expressive power regarding these aspects. Yet, they lack software tools enabling the application of efficient model checking algorithms. On the other hand, such tools exist for graphical, lower level, models such as timed automata (e.g., Uppaal) and time Petri nets (e.g., Tina).

Intermediate models are a key to bridge the gap between languages and graphical models. For instance, NTIF (New Technology Intermediate Format) was proposed to represent untimed sequential processes that handle complex data.

In this thesis, we propose a new model named ATLANTIF, which extends NTIF with real-time constructs and parallel compositions of sequential processes. Their synchronization is expressed in a simple and intuitive way using the new notion of synchronizers.

We show that ATLANTIF is capable of expressing the main constructs of high-level languages. We also present translators from ATLANTIF to timed automata (for verification using Uppaal) and to time Petri nets (for verification using Tina). Thus, ATLANTIF extends the class of systems that can practically be formally verified, which we illustrate along an example.

KEYWORDS:

automaton, concurrency, formal method, intermediate model, Petri net, process algebra, real time, verification

Back to the VASY Home Page