Rigorous Methods for Software Engineering

Part 1: SPARK

Many engineering facilities make use of water as a coolant. Storage tanks are typically used in order to maintain a sufficient supply of water. Controlling the amount of water within such water tanks can therefore represent a safety critical component of the facility. All such tanks have physical limits which if exceeded will represent a major hazard to life and/or the environment. Automated subsystems which detect such hazards and invoke corrective actions play a critical role in ensuring the overall safety of a system.

The focus of this coursework is the development of software based Water Tank Protec- tion (WTP) system. The role of WTP is to ensure that a safe level of water is maintained within the tank. Exceeding the capacity would result in a structural failure in the water tank, which in turn would cause a failure in the water supply. Conversely, if the water level gets too low then the safety of the facilities that it is cooling maybe compromised.

Specifically, your aim is to implement the software component of a simple WTP system using the SPARK 2014 approach to high integrity Ada. You are provided with SPARK package specifications that define the safety-critical boundary of the system as well as a test harness written in Ada. Your task is to develop the system-critical control component as well as the implementation details of the boundary packages. In §2.1 a system-level description of the WTP system is provided. The tasks associated with this assessment are detailed in §2.2, while the testing requirements are outlined in §2.3. Finally, in §2.4 the deliverables that are expected of you are described.

System-Level Description
The WTP system comprises of a central controller and 4 boundary subsystems that man- age the console, sensors, alarm, and an emergency drainage valve. The sensors measure the level of water within the water tank. In order to reduce the effects of component failure 3 sensors are used. Each sensor generates a value in the integer range 0cm to 2100cm inclusive. The range of valid water level values is divided into 3 categories:

LOW : value between 0cm and 99cm. NORMAL : value between 100cm and 1999cm. HIGH : value between 2000cm and 2099cm.
If a sensor reading exceeds 2099cm, i.e. a value of 2100cm, then it is deemed to be undefined (UNDEF). The sensor value returned to the WTP controller is calculated as the majority of the 3 sensor readings. For example, if two sensors give a reading of 99cm while the third gives a reading of 100cm, then the majority value is 99cm. If there does not exist a majority then an undefined value is returned to the WTP controller. If a NORMAL sensor value is returned to the WTP controller, and the alarm is not enabled, then no action is required. If a HIGH sensor value is returned to the WTP controller then the alarm is enabled. Once the alarm is enabled, if subsequent sensor readings do not show a decrease in the water-level then the WTP controller should open the emergency drainage

valve. However, if subsequent sensor readings show a decrease in the water-level then the alarm should be disabled when the water-level returns to NORMAL. If a LOW sensor value is returned to the WTP controller then the alarm is enabled. Once the alarm is enabled, if the water-level eventually returns to NORMAL then the alarm should be disabled. If a reset request is received by the WTP controller, and the water-level is below the HIGH threshold, then the WTP controller should ensure that the emergency drainage valve is closed and that the alarm is disabled.

Tasks
The safety-critical software for the WTP system is to be written in SPARK. The safety- critical functionality is to be distributed across 5 packages (subsystems) as described be- low:

Console: provides an interface to the WTP controller. Specifically it supports a reset mech- anism and is responsible for maintaining the state information on the reset subsys- tem.

Sensors: responsible for maintaining and providing access to the current values of the sensors.

Alarm: provides control of the WTP alarm and is responsible for maintaining the state information on the alarm subsystem. In addition it also counts the number of alarm events.

Drain: provides control of the water tank's emergency drainage valve and is responsible for maintaining the state information on the Drain subsystem.

WTP: responsible for the overall control provided by the WTP system.
The SPARK package specifications for Console, Sensors, Alarm and Drain can be ob- tained from:

You are required to:
T1: Develop package bodies consistent with the specifications given for Console, Sensors, Alarm and Drain. Depending upon how you define the package bodies, you may find that you need to refine the contracts within the package specifications. In addition, for each of the 4 package specifications you should add a Proof Contract to each of its subprograms, i.e. functions and procedures.
T2: Develop a WTP package (.ads and .adb) that implements the intended behaviour of the WTP controller procedure, i.e. WTP.control, as described in §2.
T3: The WTP package must be consistent with the other 4 package specifications as well as the test harness described below in §4.
T4: Using the SPARK proof tools, your SPARK code should be shown to be consistent with the Dependency Contracts.
T5: Using the SPARK proof tools, your SPARK code should be shown to be free from Run-Time Exceptions.
T6: Using the SPARK proof tools, your SPARK code should be shown to be correct with respect to the Proof Contracts.

Software Testing Requirements
You are given a test harness for the purposes of testing your WTP system software. The test harness is written in Ada (i.e. not SPARK compliant) and allows the simulation of the environment within which the WTP system is intended to operate. The test harness involves 2 packages that are described as follows:

Handler: responsible for:

1. maintaining the state information associated with the Sensors and Console packages. The state information is read from a file called env.dat (see Ap- pendix A.1).

2. logging the state information associated with Sensors, Alarm, Drain, Console as well as the majority sensor reading (category). The logger writes to a file called log.dat (see Appendix A.2).

Test WTP: responsible for running your WTP control procedure against test data (i.e. env.dat).

The actual reading of the test data and the recording of the results (i.e. log.dat) is performed by subprograms defined within the Handler.

Your submission via Canvas should include a report (Part 1 of 2) that contains the follow- ing:

D1: A statement of any assumptions you have made about the requirements, and how they have impacted on your implementation decisions.

D2: A diagrammatic representation of the software architecture of your WTP system soft- ware. Your diagram should communicate the subsystems and their local state, as well as their connectivity, i.e. imports and exports.

D3: Listings of each source file, i.e. ALL 5 packages (specifications & bodies) that define the WTP system software (see requirements). Ensure that your source files are well formatted and are readable.

D4: The summary file generated by the SPARK analysis of your code, i.e. the use of gnatprove.out in performing flow analysis and in proving exception freedom.

D5: The log.dat file generated by your WTP system software for the env.dat file given in Appendix A.1.

D6: The log.dat file generated by your WTP system software for the env.dat file given in

D7: With explicit reference to your code, describe how you protected against run-time exceptions, i.e. what you protected against and how you achieved the protection.

D8: Select a programming language that you have previous experience of, e.g. Java, C, C++, etc Focusing on language features, compare and contrast your chosen lan- guage with SPARK. Specifically describe using examples (i.e. code fragments) at least two strengths and two limitations of each language. You should aim for around 500 words (excluding example code fragments).

Each section should be clearly labeled with its deliverable number, i.e. D1, D2, D3, etc. There will be 2-marks allocated according to the clarity, quality and accessibility of Part 1 of your report. Part 1 of the coursework is worth 30 marks in total.

3 Part 2: SPIN

High pressure vessels are common place across many industrial sectors. All such vessels have physical limits which if exceeded will represent a major hazard to life and/or the envi- ronment. Automated subsystems which detect such hazards and invoke corrective actions play a critical role in ensuring the overall safety of a system.

In this coursework your task is develop a Promela model of the Automatic Vessel Pro- tection (AVP) system. In §3.1 an abstract system-level description of the AVP system is provided. The tasks associated with this assessment are detailed in §3.2. In §3.3 the deliverables that are expected of you are described.

Abstract System-Level Description

The AVP system comprises of a controller that interacts with its environment, i.e. as de- picted in Figure 1. The controller senses the monitored variables within the environment but has no direct control over them. The controller, however, influences the environment through the controlled variables.

Pressure readings in your model are to be partitioned into two categories, i.e. normal and critical. The requirements for the AVP system are as follows.

If a normal sensor value is observed by the AVP controller then no action is required. In the event of a critical sensor value being observed by the AVP controller then the alarm should be enabled and the emergency escape valve should be activated. Once the alarm is enabled and the escape valve is activated then the status of each should remain the same until a reset signal is observed.

Tasks

You are required to:

T1: Decide what the monitored variables are required and ensure that they are correctly initialized.

T2: Decide what the controlled variables are required and ensure that they are correctly initialized.

T3: Model a the environment as a proctype called env. The environment should make reasonable assumptions as to how pressure values change over time, i.e. when the escape valve is open and closed, etc. You should avoid the use of atomic state- ments.

T4: Model the controller as a proctype called control. You should avoid the use of atomic statements.

T5: Formulate an invariant as a monitor process that expresses the fact that pressure is either normal or critical at all times.

T6: Formulate an invariant as a LTL property that expresses the fact that pressure is either normal or critical at all times.

T7: Formulate a LTL response property that states that whenever the pressure is critical the escape valve is eventually opened. Verify this property using weak fairness.

T8: Formulate an LTL safety property that ensures that whenever the escape valve is open the alarm has been enabled. Verify this property using weak fairness.

Your submission via Canvas should include a report (Part 2 of 2) that contains the follow- ing:

D1: What assumptions you have made in terms of modelling the environment.

D2: State machine descriptions of your controller and its environment.

D3: Your Promela source file.

D4: Screen shots of iSpin showing the successful verification runs. Clearly state which verification parameters have be set for each verification

D5: With reference to an example Promela program, describe the notion of a race con- dition. Your answer should explain why the presence of a race condition can have an negative impact on a software system, particularly within the context of system critical systems. In addition, describe a mechanism that would eliminate the race condition from your given Promela program. You should aim for no more than 500 words (excluding code).