Design modeling and analysis of ITS using UML and Petri Nets

Design, modeling and analysis of ITS using UML and Petri Nets Fabien Bonnefoi and Lom Messan Hillah and Fabrice Kordon and Xavier Renault Abstract— This paper is about the application of formal methods to model and analyze complex systems in the context of Intelligent Transport Systems (ITS). It suggests a specification methodology based on a set of UML diagrams to generate a complete analyzable formal model. The methodology integrates the requirements of incremental and modular development for complex systems. The analysis made on the formal model is carried out through qualitative criteria, verified by model checking tools. The proposed guidelines are illustrated by a case study which considers cars in traffic situations, exchanging information about their states to reach consistency among their driving decisions. I. INTRODUCTION Transportation networks are still subject to congestion and safety problems. There is a need to improve quality, efficiency and safety on transport systems. In that context, application of formal methods on the design, modeling and analysis of Intelligent Transport Systems (ITS) can provide an appropriate framework for those improvements. ITS development is aiming at full cooperation between vehicles and infrastructures so as to take advantage of the detection and control capabilities of the vehicle ad-hoc network and the centralized infrastructure support. There is a high number of involved entities and various concurrent strategies and decisions are implemented at different levels. Therefore ITS are very complex and often imply safety- critical applications.

• such safety


• can also


• formal model


• uml


• into


• vehicle


• assembled using


• must notify adjacent