Soutenance de thèse de Fabien BONNEFOI

Bonjour,

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

"Vérification Formelle des Spécifications de Systèmes Complexes,
Application aux Systèmes de Transport Intelligents"

La soutenance se déroulera:

==========
Lundi 27 Septembre à 14h00
à l'UPMC, 4 place Jussieu
bâtiment 41, salle 203-205.
Plan:
http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/campus_jussieu2.html
==========

Vous êtes également invités au pot qui suivra.

==========
RÉSUMÉ
==========

Les Systèmes de Transport Intelligent (STI) pour la route sont
indispensables à la gestion du trafic et à la sécurité des usagers.
Complexes et critiques, leur comportement dépend de nombreux
phénomènes continus et leur
conception nécessite la collaboration de nombreuses équipes. La
vérification formelle de ces systèmes pose différents problèmes
d'intégration au cycle de développement, d'explosion combinatoire,
de vérification des phénomènes continus et de coût de production des
modèles.

En utilisant le STI SAFESPOT comme cas d'étude, cette thèse propose
différentes solutions aux problèmes d'utilisation des méthodes
formelles au cours du cycle de développement d'un système complexe.
D'abord en proposant une méthode de génération de modèles formels à
partir des spécifications du système. Nous présentons un ensemble de
règles de transformation permettant de produire des modèles formels
(en Réseaux de Petri) à partir des spécifications semi-formelles du
système (des diagrammes UML). Cela permet de minimiser le coût de
production des modèles formels tout en favorisant une bonne
communication entre les différents acteurs d'un projet.

Différents aspects de composition du modèle formel sont ensuite étudiés afin
de permettre une approche modulaire. Grâce à l'élaboration d'un
patron générique pour notre modèle formel, différents scénarios de
composition et d'analyse peuvent être effectués à moindre coût tout
en réduisant les problèmes d'explosion combinatoire.

Enfin, nous proposons une technique d'intégration de phénomènes continus
dans les modèles formels par discrétisation. Cette approche permet
la production de modèles sur lesquels les propriétés de logique
temporelle sont décidables. Nous présentons une méthode de calcul de
la propagation des incertitudes liées à la discrétisation. Ces
incertitudes peuvent ensuite être prises en compte en modifiant les
modèles ou les propriétés à vérifier afin de garantir la validité
des preuves produites.

==========
ABSTRACT
==========

Intelligent Transportation Systems (STI) for the road are
essential for traffic management and security of road users.
Complex and critical, their behavior depends on many continuous
phenomena and their design requires the cooperation of many teams.
Formal verification of these systems raises several problems like
integration into a development cycle, combinatorial explosion,
verification of continuous phenomena and production costs of models.

Using SAFESPOT ITS as a case study, this thesis proposes
different solutions to integrate formal methods in the
development cycle of a complex system.
First, by proposing a method for generating formal models
from the system specifications. We present a set of
transformation rules to produce formal models
(in Petri nets) from semi-formal specifications of
system (UML diagrams). This minimizes the cost of
production of formal models while promoting good
communication between project stakeholders.

Different aspects of composition of formal model are then studied to
allow a modular approach. With the development of a
generic pattern for our formal model, different composition
and analysis scenarios can be performed at lower cost while
reducing the problems of combinatorial explosion.

Finally, we propose a technique for integrating continuous phenomena
in formal models by discretization. This approach allows
production models on which the properties in branching-time
logic is decidable. We present a method to compute
propagation of uncertainties related to the discretization. These
uncertainties can then be taken into account by modifying
models or verification properties to ensure
the validity of produced proofs.

==========
JURY
==========

Directeur de thèse:
M. Fabrice KORDON, Professeur à l'Université Pierre et Marie Curie
Rapporteurs:
M. Yvon KERMARREC, Professeur à l'École Nationale Supérieure des
Télécommunications de Bretagne
M. Jean-Claude ROYER, Professeur à l'École des Mines de Nantes
Examinateurs:
Mme. Béatrice BÉRARD, Professeur à l'Université Pierre et Marie Curie
Mme. Christine CHOPPY, Professeur à l'Université Paris Nord
M. Guy FREMONT, Innovative solutions manager
M. Franck POMMEREAU, Professeur à l'Université d'Évry

--
___________________________________
Fabien BONNEFOI
Doctorant Paris 6 / ATER Paris 13
Université Pierre & Marie Curie
Lip6 équipe Move
Bureau 202 tours 25-26
Tél.: +33 (0) 1 44 27 39 21
___________________________________