Fabien Bonnefoi

Docteur en Informatique
Vérification & Simulation des systèmes complexes
01 43 37 26 05 bonnefoi . fabien at free . fr

Travaux de recherche et publications

Mes travaux de recherche s'articulent autour de deux axes principaux: la modélisation et le développement des systèmes de transport intelligents et la vérification formelle des systèmes complexes.

Développement des systèmes de transport intelligents pour la route

La conception, la spécification puis le développement de systèmes de transport intelligents dans le cadre de projets de recherche internationaux posent de nombreux défis en terme de méthode de développement dus à la quantité et à la diversité des partenaires d'une part, et à la complexité des systèmes à élaborer d'autre part. Parmi ces défis, on peut citer: l'analyse des besoins sur des populations variées et avec des sources d'informations hétérogènes, la gestion des contraintes spécifiques aux zones urbaines, rurales ou autoroutières, ou encore l'élaboration d'une méthode unifiée de spécification au niveau international.
Voici la liste de mes publications portant sur ces différents problèmes liés au cycle de développement des systèmes de transport intelligent pour la route:

Simulation Multi-Echelle du Trafic Routier [pdf] [présentation] [vidéo 1 : Echelles] [vidéo 2: Anti-Collision]
Fabien Bonnefoi, Julien SOULA, Ludovic Leclercq et Cécile Bécarie.
Colloque GIS MU 2012: La modélisation des flux au service de l’aménagement urbain, Lille, France, Juin 2012

From user needs to application, the SAFESPOT approach based on roads data analysis.[pdf]
Fabien Bonnefoi, Fracesco Bellotti, and Tobias Scendzielorz.
6th European Congress and Exhibition on Intelligent Transport Systems and Services, Aalborg, Denmark, June 2007.

Infrastructure-Based Co- operative Architectures: How Safespot Deals with Different Road Network Areas. [pdf]
Filippo Visintainer, Fabien Bonnefoi, Francesco Bellotti, and Tobias Scendzielorz
14th World Congress and Exhibition on Intelligent Transport Systems and Services, Beijing, China, October 2007.

SAFESPOT Applications for Infrasructure-based Co-operative Road Safety [pdf]
Fabien Bonnefoi, Francesco Bellotti, Tobias Scendzielorz, and Filippo Visintainer.
14th World Congress and Exhibition on Intelligent Transport Systems and Services, Beijing, China, October 2007.

SAFESPOT specification method: an example with infrastructure based applications [pdf]
Fabien Bonnefoi and Fahim Belarbi.
15th World Congress and Exhibition on Intelligent Transport Systems and Services, New-York, U.S.A., October 2008.

Synthèse comparative des projets Européens CVIS, SAFESPOT et COOPERS; et participation de l'A.S.F.A. [pdf]
Fabien BONNEFOI, Gwenaelle TOULMINET, Jacques BOUSSUGE et Claude LAURGEAU.
ATEC-ITS France International Congress 2009.

Vérification Formelle des Systèmes Complexes par 'model checking':

L'intérêt des méthodes formelles pour spécifier et vérifier les systèmes complexes n'est plus à démontrer. Néanmoins ces méthodes posent encore des problèmes de passage à l'echelle, de modularité ou encore de gestion des phénomènes continus au moment du calcul de l'espace d'état du modèle. Voici la liste de mes publications portant sur ces différents problèmes d'utilisation des méthodes de model checking:

An approach to model variations of a scenario: Application to Intelligent Transport Systems [pdf]
Fabien Bonnefoi, Lom Hillah, Fabrice Kordon, and Guy Frémont.
4th International Workshop on Modeling of Objects, Components and Agents. Volume 272, pages 65--86 (2006)

Design, modeling and analysis of ITS using UML and Petri Nets [pdf]
Fabien Bonnefoi, Lom Hillah, Fabrice Kordon, and Xavier Renault.
IEEE 10th International Conference on Intelligent Transportation Systems. ISBN: 1-4244-1396-6 pages 314--319 (2007)

A discretisation method from coloured to symetric net: application to an industrial example [pdf]
Fabien Bonnefoi, Christine Choppy, and Fabrice Kordon.
LNCS Transactions on Petri Nets and Other Models of Concurrency III (ToPNoC)
Lecture Notes in Computer Science,Vol. 5800, ISBN: 978-3-642-04854-8 (2009)

Sélection parmi les meilleurs papier du:
9th Workshop and Tutorial on Practical Use of Coloured Petri Nets and CPN Tools,
ISSN: 0105-8517 pages 183--202 (2008) [pdf]

Thèse - Vérification Formelle des Spécifications de Systèmes Complexes par réseaux de Petri: Application aux Systèmes de Transport Intelligents

Thèse de doctorant de l'univeersité Pierre & Marie Curie soutenue le 27 Septembre 2010
Directeur de Thèse: Pr. Fabrice Kordon
Encadrants: M. Guy Fremont & M. Fahim Belarbi

Résumé:
L’analyse formelle est le meilleur moyen de prouver tout ou partie de la logique sous-jacente d’un système ou d’un logiciel. À première vue abstraites et complexes à mettre en oeuvre, elles sont souvent considérées comme une charge de travail supplémentaire. Ainsi, pendant longtemps, leur utilisation s’est faite presque exclusivement dans les domaines exigeant un haut niveau de fiabilité comme l’armement, l’aérospatial, la cryptographie ou la sécurité informatique.
Mais alors que les domaines où l’informatique joue un rôle essentiel en termes de sécurité sont de plus en plus nombreux et les systèmes de plus en plus complexes, les méthodes de développement s’adaptent et évoluent dans le sens d’une utilisation accrue des méthodes formelles. Toutefois, l'utilisation des méthodes formelles pour la spécification et la vérification des systèmes logiciels pose encore différents problèmes.

• Les systèmes sont complexes et leur analyse pose des problèmes d'explosion combinatoire. La complexité des systèmes rend la production des modèles formels longue et coûteuse.
• Très souvent les systèmes réels mélangent des phénomènes discrets et continus constituant des systèmes « hybrides ». Les systèmes hybrides impliquent des modèles de calculs qui ne sont pas finis et il faut trouver de nouvelles solutions pour pouvoir décider des propriétés sur ces modèles.
• Le développement des systèmes nécessite la collaboration de différents acteurs, chacun spécialisé dans une partie du processus. Une bonne communication entre ces acteurs est nécessaire à l'élaboration du système. Or les modèles formels sont souvent complexes à interpréter et leur utilisation ne doit pas entraver la collaboration au sein du projet.

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 é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.
Nous proposons une méthodologie 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.
Les systèmes de transport intelligent pour la route constituent un cas d'étude intéressant pour l'évaluation de nos solutions d'intégration des méthodes formelles au cours d'un cycle de développement. Ce sont des systèmes complexes et critiques indispensable à la gestion du trafic et à la sécurité des usagers. Leur comportement dépend de nombreux phénomènes continus et leur conception nécessite la collaboration de plusieurs équipes. L'analyse formelle d'un système d'alertes aux conducteurs à différents niveaux d'abstraction nous permet de démontrer la pertinence de notre approche.

Mémoire: [pdf]
Présentation: [pdf]

modifié le 28/10/2013