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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal methods and temporal safety requirements: A level crossing application


    Beteiligte:
    Defossez, F. (Autor:in) / Bon, P. (Autor:in) / Collart Dutilleul, S. (Autor:in)


    Erscheinungsdatum :

    2007


    Format / Umfang :

    12 Seiten, 5 Bilder, 22 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Formal structuring for development of level crossing ontology

    Drewes, J. / Slovak, R. / Tordai, L. et al. | Tema Archiv | 2007


    Safety Analysis of a Radio-Based Crossing Control System Using Formal Methods

    Reif, W. / Schellhorn, G. / Thums, A. et al. | British Library Conference Proceedings | 2001


    Railway level crossing safety system

    JON OTEGUI VAN LEEUW | Europäisches Patentamt | 2019

    Freier Zugriff