Moving-block System: Requirements and Formal Models
DOI10.5281/zenodo.3375494Zenodo3375494MaRDI QIDQ6704287FDOQ6704287
Dataset published at Zenodo repository.
D. Basile, Franco Mazzanti, Alessio Ferrari
Publication date: 23 August 2019
Copyright license: Creative Commons Attribution 4.0 International
A moving-block system (cf. https://en.wikipedia.org/wiki/Moving_block) is a railway signalling and distancing system aimed at reducing the headways between trains along a track, therefore increasing line capacity. In railways, a block is intended as a segment of track that is assigned to a train: atrain cannot enter a block that is occupied by another train. With traditional fixed-block systems, each moving train is assigned a fixed block, regardless of its speed and position within the block itself. With moving-block systems, the block is dynamically computed based on the position and speed of the train, which is continuously computed onboard and communicated to the wayside control systems. This enables the possibility of routing more trains along the same track. For more details, please refer to:https://en.wikipedia.org/wiki/Communications-based_train_control The package includes a set of requirements andmodels for a railway moving-block system: (a) a PDF document named Moving-block Model and Requirements.pdf, which includes a UML model of a moving-block system together with a set of requirements for the system; (b) a set of 9 folders, each one associated to a formal or semi-formal development tool. Each folder contains one or more models of the moving-block system from (a), developed by means of the tool. The models were developed usingthe following tool versions. Other versions may still open and verify the models. Simulink(2017b) UMC(4.7) UPPAAL SMC(4.1.4) Atelier B(4.2.1) ProB(1.10.2018) NuSMV(2.6.0) SPIN(6.4.9) CADP(2019-a) FDR4(4.2.3)
This page was built for dataset: Moving-block System: Requirements and Formal Models
