ASTRail Deliverable 4.3, Task 4.4 - Supplementary Material

This package contains supplementary material for the deliverable 4.3 of the ASTRail Project: http://www.astrail.eu/ The deliverable focuses on Task 4.4 of the project, aimed at producing a verifiable specification of the moving-block train distancing system integrated with automated driving technologies (automatic train operation, ATO). The package includes the following folders: - HTML-Integrated-ATO-Moving-Block-Specification: a specification in HTML format, automatically generated from the Simulink-Stateflow model included in Simulink-Stateflow-Models > Integrated-ATO-Moving-Block-Model; Click on the file "ASTRail-Moving block and ATO.html" to visualise the document. - Simulink-Stateflow-Models: includes three separate Simulink models, namely ATO-Model (model of the ATO in isolation),  Moving-Block-Model (model of the moving block in isolation),  and Integrated-ATO-Moving-Block-Model (integrated model with moving block and ATO).  To run each model: use Simulink 2017b, or other compatible version; double click on the file with extension ".slx" included in each folder; double click on the file "ASTRail_msg_bus.mat"; start the simulation through Simulink. - Event-B-ProB-Models-and-Properties: includes five Event B models, with extension ".mch", and two .txt files with properties to be verified on the models. The models are PROB-ATO-alone-v13 (model of the ATO in isolation); PROB-MB-alone-v13 (model of the moving block in isolation); PROB-MB+ATO-v13 (integrated model with moving block and ATO) PROB-DRIVER+ATOdriverdata-v13 (DRIVER and ATO data); PROB-MB+ATOobudata-v13 (ATO and OBU data).  PROB-MB-alone-v13-properties.txt includes properties to be verified on the model of the moving block in isolation. PROB-MB+ATOobudata-v13-properties includes properties to be verified on the model including ATO and OBU data. To visualise and verify the models, use ProB version 1.9.0.