Functioning mode Management and formal assessment of safety

This paper presents a methodology to assist the safety assessment of timed discrete event systems. The methodology is illustrated on a level crossing case-study. It is a critical component for the safety of railway systems. The first step consists in decomposing the system functioning into different functioning modes. Then under specific assumptions, a model is provided for each functioning. Then, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Considering a proposed technological solution, its global functioning is also decomposed in several modes. As a latter, the model of the solution can be assessed, mode by mode. This assessment is achieved comparing the state classes deduced from the requirement model and the state classes of the proposed solution.