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.
Defence : 09/27/2010 - 14h - Site Jussieu - Bat 41 - Salle 203/205 Jury members : 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)