Moving-block System Requirements and Formal Models

The package includes a set of models 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 model of the moving-block system from (a), developed by means of the tool. The models were developed using the 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)