Level crossing is a critical component of the European railway network. The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level reliability and correctness must be reached by the use of mathematical proofs and then formal methods. As the time specifications are difficult to deal with, this paper proposes to apply a dedicated modelling tool. The authors explained the ability of p-time Petri net to specify temporal requirements. In order to illustrate the tool adequacy, the authors modelled a level crossing benchmark. It is based on Petri nets translation to automata in order to analyse the benchmark. Moreover, the analysis is provided in order to specify a safe control even if there are interoperability problems with the radio signal. In order to integrate this methodology in the global problematic of safety requirements, the authors propose an approach based on high level Petri nets, of which p-time Petri nets are a subclass. The authors have presented the perspective of the use of a process allowing the complementary strengths of the B formal method and the Petri net model to be used together in order to promise increased reliability of a railway traffic control application. The aim is to provide some sharp results concerning time parameters and a global approach including all functional aspects.
Formal methods and temporal safety requirements: A level crossing application
2007
12 Seiten, 5 Bilder, 22 Quellen
Aufsatz (Konferenz)
Englisch
Formal structuring for development of level crossing ontology
Tema Archiv | 2007
|Safety Analysis of a Radio-Based Crossing Control System Using Formal Methods
British Library Conference Proceedings | 2001
|Application of safety management process for the safety analysis of level crossing
Tema Archiv | 2005
|