Rigorous Methods for Software Engineering

A SPIN Design Modelling and Verification Exercise

A SPIN Design Modelling and Verification 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

Modelling Tasks

In terms of modelling, your task is to extend the Promela model given in Figure 2 so as to guarantee the safe passage of trains, i.e. so that the safety property given in §2 holds. Your design must adhere to the following constraints:

mtype = { T1, T2 }

chan TunnelAB = [2] of { mtype }; chan TunnelBC = [2] of { mtype }; chan TunnelCD = [2] of { mtype }; chan TunnelDA = [2] of { mtype };

proctype Station(chan exit_tunnel, enter_tunnel)
{
byte train; do
:: exit_tunnel?train; enter_tunnel!train; od
}

proctype Setup(chan tunnel; byte train)
{
tunnel!train;
}

init { atomic{
run Setup(TunnelBC, T1); /* introduce train T1 before station C */ run Setup(TunnelDA, T2); /* introduce train T2 before station A */ run Station(TunnelDA, TunnelAB); /* station A */
run Station(TunnelAB, TunnelBC); /* station B */ run Station(TunnelBC, TunnelCD); /* station C */ run Station(TunnelCD, TunnelDA);} /* station D */
}

A simple metro network involving four stations and four tunnels is modelled. The metro network is circular with all the stations separated by tunnels. While each station is modelled by a process, the tunnels are modelled by channels. Consequently the movement of trains is modelled by message passing, where a train is denoted by a unique identifier, i.e. T1 or T2. While trains only travel in one direction, the network is unsafe because trains may travel at different rates. Within the model, a crash (unsafe state), corresponds to two trains occupying the same tunnel at the same moment in time. Note that a two train network, as modelled here, is sufficient to demonstrate that the system is unsafe. Note also that the role of the Setup process is to simply introduce a train in the network.

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.
Hint: a signal box process will obviously have to remember whether or not a train is cur- rently within its area of control. Consequently, when your system model is initialized, the signal box processes will need to be instantiated with information about the position of trains within their area of control within the network, i.e. to prevent a train proceeding into a tunnel that is already occupied by another 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 prop- erty given in §2.
T9: Using a temporal property, verify that your system design satisfies the safety prop- erty 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.

Deliverables
Your submission via Canvas should take the form of i) a report and ii) a standalone text file containing your Promela code. Your report must include the following:
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. [ 1 mark ]

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. [ 5 marks ]

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