Case Study: Verification of an Embedded Fault-Tolerant Avionics System
Brockmeyer, U. and Wittich, G.
IEEE International Workshop on Embedded Fault-Tolerant Systems (EFTS'98)
This paper shows how an fault-tolerant avionics system given as a STATEMATE design can be verified using a toolset we built. We demonstrate our verification environment on a sample avionics case study which is provided by our project partner ESG. This case study is about a fault-tolerant Helicopter Monitoring System of a Helicopter with two engines. There are two independent tasks which are scheduled periodically by a control task. For each engine the first task compares a computed and a measured rotations per minute (rpm) value. If the difference raises above a given threshold, the task generates an alarm displayed to the pilot. Then the pilot has to decide whether to switch off the engine or not. The second task monitors the remaining fuel of the aircraft. It first computes two values to determine the remaining amount of fuel. One value is computed by fuel throughput and one is computed by the initial amount of fuel and the flight distance. Again an alarm is generated if the two values differ too much. Otherwise the weighted average of these values is assumed to be the remaining amount of fuel. An alarm is also generated if this value reaches a critical threshold. All generated alarms have to be acknowledged by the pilot. The control task schedules the above two tasks and also accepts commands given by the pilot by performing the corresponding actions. We present some results we got on verifying some relevant properties of the fault-tolerant monitoring system with our toolset.
01 / 1998
inproceedings
90-95
