English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

14th International Conference on Railway Engineering Design and Optimization (COMPRAIL 2014), Rome, ITALIE, 24-/06/2014 - 26/06/2014A railway interlocking system (RIS) plays a vital role in the safe transportation of a railway system. It is responsible for the safe routes of trains making sure that each train movement follows the other in a proper and safe sequence. Detailed verifications and evaluations are mandatory before deploying an RIS, since it is a safety critical system (SCS). But the increasing complexity of the RIS tends to limit the capability of the classic approval methods. As a result, the formalization of RIS becomes important to both the development of computer interlocking software and the third-party testing of the RIS facilities. Petri nets are a powerful formal tool that have been applied to many railway applications. Considering the large scale and the space complexity of interlocking systems, this paper introduces a feasible method for modeling the RIS by hierarchical colored Petri net (HCPN), which aim at providing a formal verification and logic evaluation of the French RIS. The paper describes how the signaling control logical and the railway road layout are specified and constructed into the HCPN. First, the architecture of RIS and the hierarchical structure of the model framework are introduced. Then, several basic RIS components are established as Petri nets to illustrate how to map RIS components into HCPN. As a case study, a section of a typical French station is modeled. It includes interlocking routes and signaling control principles. This paper takes place in the framework of the ANR project 'PERFECT'. As this method has already received recognition from French railway experts, the future research contains consistency checking with some other parts of the specification, such as operation rules, which allows us to find out the crux of some existing problems and to discover some potential safety hazards. Keywords: railway interlocking system, modeling methodology, hierarchical colored Petri net

A formal modeling methodology of the French railway interlocking system via HCPN