Soutenance de thèse de Damien Thivolle

Damien Thivolle a soutenu le 29 avril 2011 à 11h00
dans l'Amphithéâtre EG 301 de l'Université Polytechnique de Bucarest
313 Splaiul Independentei, Bucarest, Roumanie

une thèse de doctorat de l'Université de Grenoble et de l'Université Polytechnique de Bucarest,
spécialité : informatique, intitulée :

"Langages modernes pour la modélisation et la vérification des systèmes asynchrones"

Thèse préparée dans le Centre de Recherche INRIA Grenoble Rhône-Alpes, au laboratoire LIG (équipe-projet VASY) et au laboratoire d'Informatique de l'Université Polytechnique de Bucarest
sous la direction de M. Hubert GARAVEL et de M. Valentin CRISTEA.

COMPOSITION DU JURY :

  • M. Dumitru POPESCU, professeur à l'Université Polytechnique de Bucarest (président du jury)
  • M. Ioan JURCA, professeur à l'Université Polytechnique de Timisoara (rapporteur)
  • M. Charles PECHEUR, professeur à l'Université Catholique de Louvain (rapporteur)
  • Mme Mihaela SIGHIREANU, maître de conférences à l'Université Paris-Diderot (examinateur)
  • M. Hubert GARAVEL, directeur de recherche à l'INRIA Grenoble - Rhône-Alpes (directeur de thèse)
  • M. Valentin CRISTEA, professeur à l'Université Polytechnique de Bucarest (codirecteur de thèse)



Manuscrit (282 pages)
PDF
PS
Transparents de la soutenance
PDF

RESUME :

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes.

Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets :

  1. Pour les systèmes GALS (Globalement Asynchrone, Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par Airbus : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par Airbus.
  2. Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL.

MOTS-CLES : Ingénierie dirigée par les modèles, méthodes formelles, vérification, LOTOS NT, CADP, systèmes critiques, systèmes GALS, Services Web, BPEL.

Slides presented by Damien Thivolle during the PhD defense

TITLE: Modern Languages for Modelling and Verifying Asynchronous Systems

ABSTRACT:

The work in this thesis is at the intersection of two major research domains: Model-Driven Engineering (MDE) and formal methods, and has various fields of application. This thesis deals with the formal verification of parallel applications modelled by the MDE approach. In this approach, models play a central role and enable to develop an application through successive transformations (automated or not) between intermediate models of differing levels of abstraction, until executable code is produced. When models have a formal semantics, the application can be verified, either automatically or semi-automatically. These principles are used in TOPCASED, an ECLIPSE-based development environment for critical embedded applications, which enables formal verification by interconnecting existing tools.

This thesis implements the TOPCASED approach by relying on the CADP toolbox for verifying systems, and on its most recent input formalism: LOTOS NT. This thesis tackles the formal verification of MDE applications through two real problems:

  1. For GALS (Globally Asynchronous, Locally Synchronous), a generic verification method, based on a transformation to LOTOS NT, is proposed and illustrated by an industrial case-study provided by Airbus: a communication protocol between the airplane and the ground described in the synchronous langage SAM designed at Airbus.
  2. For Web services specified with the BPEL (Business Process Execution Language norm, a verification method is proposed. It is based on a BPEL to LOTOS NT transformation which takes into account XML Schema, XPath, and WSDL, the languages on which the BPEL norm is built.

KEYWORDS: Model-Driven Engineering, formal methods, verification, LOTOS NT, CADP, critical systems, GALS systems, Web services, BPEL.

Back to the VASY Home Page