ASTRail Deliverable 4.3, Task 4.4 - Supplementary Material

<p>This package contains supplementary material for the deliverable 4.3 of the <strong>ASTRail Project</strong>: <a href="http://www.astrail.eu/">http://www.astrail.eu/</a><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).</p> <p>The package includes the following folders:</p> <p>- <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 &quot;ASTRail-Moving block and ATO.html&quot; to visualise the document.</p> <p>- <strong>Simulink-Stateflow-Models:</strong> includes three separate Simulink models, namely ATO-Model (model of the ATO in isolation),&nbsp;<br> Moving-Block-Model (model of the moving block in isolation),&nbsp;<br> and Integrated-ATO-Moving-Block-Model (integrated model with moving block and ATO).&nbsp;<br> To run each model: use Simulink 2017b, or other compatible version;<br> double click on the file with extension &quot;.slx&quot; included in each folder; double click on the file &quot;ASTRail_msg_bus.mat&quot;;<br> start the simulation through Simulink.</p> <p>- <strong>Event-B-ProB-Models-and-Properties:</strong> includes five Event B models, with extension &quot;.mch&quot;, 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).&nbsp;<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> &nbsp;</p>