A SPIN Design Modelling and Verification Exercise - Rigorous Methods for Software Engineering

PROJECT

While discussion with fellow students as to the general nature of this project is acceptable, it is critically important that the solution you adopt as well as the associated code and report are completely your own work. The re-use of other peoples code (other than the code provided as part of this coursework) is not permitted and if identified will be treated as a disciplinary matter. Information on plagiarism can be found via

Safety should be the primary concern when building a railway network. The safety of a railway network typically depends upon the use of track-side signals in regulating the safe passage of trains. Establishing the correctness of the systems that control the track-side signals therefore plays a crucial role in ensuring the safety of the railway network. The aim of the coursework is to develop a formally verified design of a distributed railway signalling system. The starting point is a Promela model of a simple, but unsafe railway network. Your task is to design a distributed signalling system that will make the network safe. While the coursework does not require you to model an existing signalling system, the interested reader may find the following references useful [1, 2].

In §2 the unsafe network is described, while the modelling and verification tasks are described in §3 and §4 respectively. Finally, in §5 the deliverables that are expected of you are described. Note that this coursework counts for 30% of your overall course mark.

T1: No part of the original model can be removed, i.e. the design of your signalling system should simply add additional constraints to the existing model.
T2: Your design should take the form of a distributed communicating system, i.e. the control imposed by your signalling system should be distributed around the network. A single central signalling system is not acceptable.
T3: Each station should include a track-side signal. The role of the track-side signal is to control access to the tunnel in advance of the station.
T4: Each track-side signal should be controlled by an associated signal box.
T5: Each signal box should only be able to communicate to the signal boxes in advance and to the rear of its position, e.g. Signal Box A can only communicate with Signal Boxes B and D.
T6: A station and its associated signal box may communicate, e.g. Station A may com- municate with Signal Box A. However a station may not communicate with any other station or any signal box except for the one with which it is associated.
T7: A station and its associated signal box can only observe trains as they exit and enter their associated tunnels. That is, they are not able to see inside the tunnels. Warn- ing: the station and signal box processes should not use len, full, nfull or empty in order to determine the safe passage of a train.

Verification Tasks

Using iSPIN's reasoning capabilities you are required to undertake the following verification tasks:
T8: Using a system assertion, verify that your system design satisfies the safety property given in §2.
T9: Using a temporal property, verify that your system design satisfies the safety property given in §2.
T10: Define a response property that involves the passage of a train through a tunnel.

Verify that your system design satisfies your response property.

D0: A signed Student Declaration of Authorship form.

D1: A statement of any assumptions you have made about the informal system-level de- scription given in §2.

D2: A diagrammatic representation of your distributed signalling system, i.e. a refinement to Figure 1 that reflects your design. In addition, provide a high-level description of the how your distributed signalling system ensures the safe passage of trains in the network.

D3: The Promela source code for your system design.

D4: For each verification effort you should include the property that was verified together with a transcript of the associated "Verification Output" window.

D5: The Therac-25 radiation therapy machine contained two software bugs. One was highlighted in the introductory lecture while both are described in:
"Medical Devices: The Therac-25", N. Leveson, 1999.

Note that this paper is available on Canvas. In section 2.5.3 (pages 22-28) of the above paper the second bug is described. Your task is to describe how the second bug could have been detected using Promela and Spin. You should aim for around 500 words (excluding example code fragments)

Attachment:- Rigorous Methods for Software Engineering.rar