This verification benchmark was adapted from [GiKJ97] which in turn used the implementations discussed in [Jose96] where the example was studied using different approaches. The Quartz program considered here as a small verification benchmark describes the controller of a mine pump that must maintain the water level in a mine between minimum and maximum levels as water continuously percolates into the mine. To this end, the controller switches the pump on when the water level reaches the high water level and switches it off when the water level falls below the low water level. The controller consists of the following parallel components:
The controller has the sensors A,B,C,D,E (shown in the following figure) which provide boolean valued inputs as listed below. Additionally, there is a human operator with limited rights who can press buttons to manually switch the mine pump on or off, and the is also a human supervisor with unlimited rights who can also press buttons to manually switch the mine pump on or off. Therefore, the controller has the following inputs:
SensorCriticCO (A) holds iff the carbon monoxide level is critical.SensorMethaneHgh (B) holds iff the methane level is too high.SensorCriticAir (C) holds iff the air flow is critical.SensorWaterHgh (D) and SensorWaterLow (E) hold if the current water level is above the high and low water level, respectively.SVStopPump and SVStartPump hold if the supervisor presses buttons to switch the pump off/on.OPStopPump and OPStartPump hold if the operator presses buttons to switch the pump off/on.Alarm must be signalled if SensorCriticCO, SensorCriticAir or SensorMethaneHgh & SensorWaterHgh holds since humans must be evacuated in these cases (methane is not toxic, but there is the risk of explosion if the mine pump is on which is required if the water level is above the high level)StartPump switches the mine pump on which must not happen if the methane level is high. If the methane level is not high, then StartPump may hold for three reasons:
StopPump switches the mine pump off which may happen for the following reasons:
PumpOff and PumpOn signal the current status of the mine pump, being either off or on.SwitchOffPump and SwitchOnPump are events which hold when the mine pump is switched off/on, i.e., changes from
PumpOn to PumpOff or vice versa.
MethaneCritical and MethaneUnCritical hold if SensorMethaneHgh is true or false, respectively.WaterLevLow, WaterLevMid, and WaterLevHgh hold if the water level is below the low water level, between the low and high water levels, or above the high water level, respectively.As mentioned above, the mine pump controller consists of five components that run in parallel. They are described briefly below.
This component signals the status of the mine pump which can be either PumpOff or PumpOn. It switches from PumpOff to PumpOn if StartPump & !StopPump holds and signals the transition by SwitchOnPump. Similarly, it switches from PumpOn to PumpOff if StopPump holds and signals the transition by SwitchOffPump. Initially, PumpOff holds.
This component controls the start/stop buttons used by the human supervisor and operator. It produces signals StartPump and StopPump when the corresponding buttons are pressed. However, the start button has a higher priority, and the human operator cannot override the supervisor's commands or perform actions if the water level is too low or too high.
This component signals Alarm if either SensorCriticCO or SensorCriticAir holds. It does not affect the control of the mine pump further.
Sensors D and E in the above figure provide inputs SensorWaterLow and SensorWaterHgh which are true if the current water level is above the low water level and above the high water level, respectively. Hence, SensorWaterHgh implies SensorWaterLow, and the controller determines three additional signals WaterLevLow, WaterLevMid, WaterLevHgh which hold if the water level is below the low water level, between the low and high water levels, or above the high water level, respectively. The water monitor signals StopPump if the water level is below the low water level, and it signals StartPump if the water level is above the high water level and the methane level is not high. Finally, it signals Alarm if the water level is above the high water level and the methane level is high.
This component monitors the methane level. If a rising edge is detected on SensorMethaneHgh, signal StopPump is raised to stop the pump (if it is running) and signal Alarm is raised if WaterLevHgh holds. If there is a falling edge on SensorMethaneHgh, signal StartPump is raised to start the pump if WaterLevHgh holds.
The main specifications that must be verified for the controller are as follows:
Alarm must be signalled whenever SensorCriticCO, SensorCriticAir, or SensorMethaneHgh&WaterLevHgh holds.SensorMethaneHgh is true.SensorWaterLow is false.SensorMethaneHgh is true.SensorWaterLow is false.SensorMethaneHgh is false and SensorWaterLow is true.SensorMethaneHgh is false and SensorWaterLow is true.