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.

Publications 2006-2010

• 2010
  • F. Bonnefoi : “Vérification Formelle des Spécifications de Systèmes Complexes, Application aux Systèmes de Transport Intelligents”, soutenance de thèse, soutenance 27/09/2010, direction de recherche Kordon, Fabrice (2010)
• 2009
  • F. Bonnefoi, Ch. Choppy, F. Kordon : “A Discretization Method from Coloured to Symmetric Nets: Application to an Industrial Example”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 5800 (III), Lecture Notes in Computer Science, pp. 159-188, (Springer) (2009)
• 2008
  • F. Bonnefoi, F. Belarbi : “SAFESPOT Specification Method: an Example with Infrastructure Based Applications”, 15^th World Congress and Exhibition on Intelligent Transport Systems and Services, New-York, United States (2008)
  • F. Bonnefoi, Ch. Choppy, F. Kordon : “A Discretization Method from Coloured to Symmetric Nets: Application to an Industrial Example”, 9^th International workshop on Practical Use of Colored Petri Nets and the CPN Tools (CPN' 08), Aarhus, Denmark, pp. 183-202, (Daimi University, PB 588) (2008)
• 2007
  • F. Bonnefoi, F. Bellotti, T. Scendzielorz, F. Visintainer : “Infrastructure-Based Co-operative Architectures: How Safespot Deals with Different Road Network Areas”, 14^th World Congress and Exhibition on Intelligent Transport Systems and Services, Beijing, China (2007)
  • F. Bonnefoi, F. Bellotti, T. Scendzielorz, F. Visintainer : “SAFESPOT Applications for Infrasructure-based Co-operative Road Safety”, 14^th World Congress and Exhibition on Intelligent Transport Systems and Services, Beijing, China (2007)
  • F. Bonnefoi, L. Hillah, F. Kordon, X. Renault : “Design, Modeling and Analysis of ITS using UML and Petri Nets”, 10^th International IEEE Conference on Intelligent Transportation Systems, Seattle, WA, United States, pp. 314-319, (IEEE) (2007)
  • F. Bonnefoi, F. Bellotti, T. Scendzielorz : “From User Needs to Application, the SAFESPOT Approach Based on Roads Data Analysis”, 6^th European Congress and Exhibition on Intelligent Transport Systems and Services, Aalborg, Denmark (2007)
• 2006
  • F. Bonnefoi, L. Hillah, F. Kordon, G. Fremont : “An Approach to Model Variations of a Scenario: Application to Intelligent Transport Systems”, Fourth International Workshop on Modelling of Objects, Components and Agents (MOCA '06), Turku, Finland, pp. 65-86 (2006)