LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Actualité » Doctorants

BONNEFOI Fabien

Docteur
Équipe : MoVe
Date de départ : 01/03/2011
http://bonnefoi.fabien.free.fr
Direction de recherche : Fabrice KORDON

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

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.
Soutenance : 27/09/2010 - 14h - Site Jussieu - Bat 41 - Salle 203/205
Membres du jury :
Fabrice Kordon (UPMC)
Yvon Kermarrec (Telecom Bretagne) [Rapporteur]
Jean-Claude Royer (Univ. Nantes) [Rapporteur]
Béatrice Bérard (UPMC)
Christine Choppy (Univ. Paris 13)
Guy Fremont (SANEF)
Franck Pommereau (Univ. Evry-Val-d'Essone)

Publications 2006-2010

 Mentions légales
Carte du site |