Safety properties modelling

In critical applications regarding safety, a solution must be validated before it is applied on the field. It is forbidden to test solutions directly on the real system for safety reasons. Any attempt of modification or introduction of a safety system must be approached with the utmost care. The proposed solutions must be validated, and, if possible, formally validated. It is the case of prevention systems for accidents, installed on highways. They also are in charge of gathering information in the case of an accident actually occurring. In this context, we aim to provide an approach to validate the behaviour of a critical system before its effective realisation. The system is modelled by a combination of agents spread around the world and working together in real-time. The agents' behaviour is modelled via an UML SysML model. Thanks to the tools available in the TTool environment and the ones developed only for this purpose, we can animate those agents and confirm, or not, their behaviour on various test situations (applications' rapid prototyping). Since the tests are not covering all the possibilities, we move to, then, verify formally the critical properties. This formal analysis is made possible by the mathematical grounds of the tool we use. The analysed properties are mainly safety properties; results regarding performance results are available as well.