ASTRail Deliverable 4.3, Task 4.4 - Supplementary Material

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