Supervision : Fabrice KORDON

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

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.

2006-2010 Publications

• 2010
  • F. Bonnefoi : “Vérification Formelle des Spécifications de Systèmes Complexes, Application aux Systèmes de Transport Intelligents”, thesis, phd defence 09/27/2010, supervision 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)