The Wireless Fire Alarm System: 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 verication of such systems is not only possible, but practicable even in the context of small to medium-sized enterprises. We considered a wireless re alarm system and uncovered severe design aws. For an improved design, we provided dependable verication 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 speci ed by generalized test procedures, then verifying that a system will pass any test following these test procedures is a cost-ecient approach to improve product quality based on formal methods.