Ensuring Conformance to Industrial Standards through Formal Verification
The design of distributed, safety critical real-time systems is challenging due to their high complexity, the potentially large number of components, and complicated requirements and environment assumptions.
Our case study shows that despite those challenges, the automated formal verification of such systems is not only possible, but practicable even in the context of small to medium-sized enterprises. We considered a wireless fire alarm system and uncovered severe design flaws. For an improved design, we provided dependable verification results which in particular ensure that conformance tests for a relevant regulation standard will be passed.
In general we observe that if system tests are specified by generalized test procedures, then verifying that a system will pass any test following these test procedures is a cost-efficient approach to improve product quality based on formal methods.
Description
We analyzed a communication protocol developed for use in the fire alarm systems of Security Care GmbH.
Several aspects of the communication protocol were analyzed according to the norm EN-54:
- The self-monitoring function
- The loss of the ability of the system to transmit a signal from a component to the central unit is detected in less than 300 seconds and displayed at the central unit within 100 seconds thereafter.
- The alarm function
- A single alarm event is displayed at the central unit within 10 seconds.
- Two alarm events occurring within 2 seconds of each other are each displayed at the central unit within 10 seconds after their occurrence.
- Out of exactly ten alarms occurring simultaneously, the first should be displayed at the central unit within 10 seconds and all others within 100 seconds.
- Protocol robustness
- There must be no spurious displays of events at the central unit.
- All requirements must hold as well in the presence of radio interference by other users of the frequency band. Radio interference by other users of the frequency band is simulated by a jamming device specified in the standard.
Additional Materials
- UPPAAL Models of the Monitoring Mechanism (copyright - all rights reserved) [ZIP]
- UPPAAL Models of the Alarm mechanism for a fixed topology
- Cascade: 5 Repeaters and 10 Sensors (simultaneous alarms) (copyright - all rights reserved) [ZIP]
- Cascade: 5 Repeaters and 2 Sensors (alarms within 2s) (copyright - all rights reserved) [ZIP]
Publications
Main Paper
Feo-Arenis, S., Westphal, B., Dietsch, D., Muñiz, M., Andisha, S. The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification. FM 2014. [PDF] [DOI] [bibTeX]
Student Projects
- Andisha, S. [PDF]
- SPIN Models of the alarm resolution protocol (copyright - all rights reserved) [ZIP]