Soutenance de thèse de Lom Hillah

Bonjour,

J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée :

«Intégration des méthodes formelles au développement dirigé par les
modèles pour
la conception et la vérification de systèmes et applications répartis»

ainsi qu'au pot qui suivra. La soutenance aura lieu le
mercredi 23 septembre à 14h au LIP6 (Site Passy-Kennedy), en salle 549.
Comment aller au LIP6 ? http://www.lip6.fr/informations/comment.php

La thèse sera soutenue devant le jury composé de :

Mme Isabel Demongodin (Université de Aix-Marseille) - Rapporteur
M. Michel Lemoine (ONERA) - Rapporteur
M. Claude Girault (Université Pierre et Marie Curie)- Examinateur
Mme Marie-Pierre Gervais (Université Paris Ouest Nanterre La Défense)
- Examinateur
M. Fabrice Kordon (Université Pierre et Marie Curie) - Directeur
Mme Laure Petrucci (Université Paris 13) - Examinateur
M. Ekkart Kindler (Technical University of Denmark) - Examinateur

=========
Résumé
=========
Nous intégrons à la démarche de développement dirigé par les modèles
(MDD),
une approche mettant fortement en oeuvre les méthodes formelles pour
la vérification de systèmes complexes. Le MDD, largement répandu dans
l'industrie, est
notamment mis en oeuvre pour le développement des systèmes de
transport intelligents (ITS).
Notre approche est motivée par le besoin de maîtriser les
spécifications comportementales
de tels systèmes et ainsi garantir leur sûreté. Elle s'articule selon
trois aspects.

Le premier aspect concerne la recherche de stratégies de contrôle pour
la supervision de systèmes
devant satisfaire une spécification donnée. Il s'agit de restreindre
leur comportement
par un contrôleur (s'il existe et peut être synthétisé) afin d'éviter
les états dangereux.
Le problème de l'explosion combinatoire de l'espace d'état nous oblige
à mettre en oeuvre
une structure de données performante comme les diagrammes de décisions
hiérarchiques.
Nous appliquons la recherche de stratégies de contrôle à l'évitement
de collisions sur
route automatisée.

Le deuxième aspect porte sur la vérification formelle de
spécifications comportementales
d'applications ITS en diagrammes d'activité UML. Les réseaux de Petri
constituant le
modèle formel le plus proche de ces diagrammes, nous les avons adaptés
aux
concepts orientés objet d'UML via la définition des Instantiable Petri
Net (IPN).
Les IPN intègrent la notion de type et d'instance de type, gèrent la
modularité et la hiérarchie.
Nous appliquons cette démarche à une application du projet européen
SAFESPOT.

Enfin, le troisième aspect concerne l'interopérabilité des outils de
réseaux de Petri
pour l'échange de modèles. Cette interopérabilité doit aider les
démarches de vérification comme
celle proposée plus haut, à élargir à faible coût la portée de la
vérification sur différents
aspects comportementaux d'un même système. Le problème de
compatibilité sémantique au niveau des différents
types de réseaux de Petri et des formats propriétaires supportés par
ces outils nous incite à
élaborer un cadre normalisé pour l'échange. C'est ainsi que nous
définissons, au sein de la norme
ISO/IEC 15909, le format d'échange Petri Net Markup Language, (PNML),
dans un cadre sémantique
unifiant les définitions des réseaux de Petri place/transition et
colorés.

==========
Abstract
==========
We integrate into the framework of Model-Driven Development, widely
adopted in the industry,
a formal methods approach for the verification of complex systems,
like intelligent
transport systems. This approach is driven by the need to control the
behavioral
specification of such systems. It is structured in three parts.

The first part is about searching for control strategies to supervise
systems that must
stay within the set of their admissible behaviors. To tackle the state
space explosion problem,
we use set decision diagrams, very compact and performant data
structures.
In this approach we look for collision avoidance strategies on an
automated highway.

The second part is about formal verification of behavioral
specifications of ITS applications
in UML activity diagrams. Petri nets being the closest formal models
to these diagrams, we
have tailored them to meet UML object-oriented concepts by defining
Instantiable Petri Nets (IPN).
IPNs encompass the notions of type, instance and they handle
modularity and hierarchy.
In this approach we verify the design of a software of the european
project SAFESPOT.

The last part is about Petri nets tools interoperability over Petri
net models.
This long-sought interoperability is meant to help easily extend the
verification
range of interesting behavioral characteristics of a system, using
different specialized tools.
The semantic compatibility issue over different Petri nets types and
proprietary supporting
formats between the tools made us set up a standardized framework for
models interchange. We thus
define the interchange format Petri Net Markup Language (PNML), second
part of the
international standard ISO/IEC 15909. It relies upon the explicit
semantic unification
of place/transition and colored Petri nets definitions.

Meilleures salutations,

Lom Messan Hillah
--------°°°----------------°°°---------------------------------------
Université Pierre et Marie Curie - UMR CNRS 7606
Laboratoire d'Informatique de Paris 6 / MoVe
tél: + 33 1 44 27 87 71 - Bureau 816
104 Avenue du Président Kennedy
75016 Paris - France
http://lip6.fr/Lom-Messan.Hillah/
--------°°°----------------°°°---------------------------------------