Rigorous Methods for Software Engineering

Coursework - A SPARK High Integrity Software Development Exercise

Tasks

The safety-critical software for the BSCU is to be written in SPARK. The safety-critical functionality is to be spread across 6 packages (subsystems) as described below:

Sensors: responsible for maintaining the state of the brake pedal and provides the BSCU controller with feedback on the brake pedal state.
Brakes: responsible for maintaining the state of the car's physical brakes and provides the BSCU controller with control of the car's physical brakes.
Alarm: responsible for maintaining the state of the car's audible/visual alarm and provides the BSCU controller with control of the car's audible/visual alarm. In addition, Alarm is responsible for maintaining a count of the number of alarm events that occur.
Speedo: responsible for maintaining the state of the car's current speed and provides the BSCU controller with feedback on the car's current speed.
Reset: responsible for maintaining the state of the reset mechanism and provides the BSCU controller with feedback on the state of the reset mechanism.
BSCU: in collaboration with above subsystems, BSCU responsible for the overall manage- ment of the car's braking capability.

SPARK package specifications (.ads) for Sensors, Brakes, Alarm, Speedo, Reset are avail- able from:

You are required to undertake the following 5 tasks:

T1: Develop package bodies consistent with the specifications given for Sensors, Brakes, Alarm, Speedo and Reset. Depending upon how you define the package bodies, you may find that you need to refine the dependency contracts within the package specifications. In addition, for each of the 5 package specifications you should add a proof contract (i.e. Pre and Post conditions) to each of its subprograms, i.e. functions and procedures.

T2: Develop a BSCU package (.ads and .adb) that implements the intended behaviour of the BSCU controller procedure, i.e. BSCU.controller, as described in §2. You should include both a dependency contract and a proof contract for BSCU.controller. Hint: for the proof contract, use the invariant property described in §2 regarding the state of the Alarm and the Brakes, i.e. a property that should be provably true before and after every execution of BSCU.controller.

T3: Ensure that your BSCU package is consistent with the 5 given package specifications as well as the test harness described below in §4.

T4: Use the SPARK proof tools to show that your code is consistent with the dependency contracts, i.e. use gnatprove in flow mode.

T5: Use the SPARK proof tools to show that your code is free from run-time exceptions and that your code is correct with respect to the proof contracts, i.e. use gnatprove in prove mode.

Software Testing Requirements

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

Env: responsible for maintaining the state information associated with the Sensors, Speedo and Reset packages. The state information is read from a file called env.dat (see appendix A.1).

Log: responsible for logging the state information associated with Sensors, Speedo, Alarm, Brakes, Reset as well as the majority sensor reading. The logger writes to a file called log.dat (see appendix A.2).

Test BSCU: responsible for running your BSCU controller 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 Env and Log packages respectively.
Note that the code for these 3 packages is provided in:
Example env.dat and log.dat files are also given in this directory.

Deliverables

Your submission via Canvas should take the form of i) a report and ii) a ZIP file containing your SPARK 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, and how they have impacted on your design decisions. Note that we are not looking for a restatement of the given description. We are looking instead for any additional information that you believe is required in order to improve the consistency and completeness of the given system-level description.
D2: A diagrammatic representation of the software architecture of your BSCU software. 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 6 packages (both specifications & bodies) that define the BSCU software. Ensure that your source files are well formatted and are readable.
D4: The summary file generated by gnatprove using flow mode when analyzing ALL the SPARK code for your BSCU, i.e. the gnatprove.out file.
D5: The summary file generated by gnatprove using prove mode when analyzing ALL the SPARK code for your BSCU, i.e. the gnatprove.out file.
D6: The log.dat file generated by your BSCU system software for the env.dat file
D7: The log.dat file generated by your BSCU system software for the env.dat file
This env.dat file will be made available by the end of week 5.

D8: 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.

D9: 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 strengthens and two limitations of each language. You should aim for around 500 words (excluding example code fragments).

There will be 2-marks allocated according to the clarity, quality and accessibility of your report. Note that this coursework counts for 30% of your overall course mark.