WATER PUMP PROJECT (High Integrity Systems)
Project Description
This project concerns the use of the SPARK (Ada-like) language and tools for annotating existing code and using the automated analysis tools.
The scenario for this project is a water tank which is collecting rainwater. The tank has a pump attached to it, which is to be used to take water from the tank when it is approaching full. The pump will fail if there is no water to pump, so it must be closed when the water level is approaching empty.
The control system is arranged into a number of packages. The Ada code for these packages is provided. The aim of the project is first to write a short summary of the role of each package, and then to add SPARK annotations to the code.
You can find detailed information in the attached files.
Tools
You can download free versions of the tools for implementing the project from the following web site: http://libre.adacore.com/libre/download2
Deadline
January 10th, 2011
Important Notes
All candidate workers are requested to answer the following questions when bidding:
1. How familiar are you with SPARK and/or GPS?
2. How familiar are you with Ada?
3. How many days will you need in order to provide the deliverables?
