TY - GEN
T1 - The wireless fire alarm system
T2 - 19th International Symposium on Formal Methods, FM 2014
AU - Feo-Arenis, Sergio
AU - Westphal, Bernd
AU - Dietsch, Daniel
AU - Muñiz, Marco
AU - Andisha, Ahmad Siyar
PY - 2014/1/1
Y1 - 2014/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84958542191&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-06410-9_44
DO - 10.1007/978-3-319-06410-9_44
M3 - Article in proceeding
AN - SCOPUS:84958542191
SN - 9783319064093
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 658
EP - 672
BT - FM 2014
PB - Physica-Verlag
Y2 - 12 May 2014 through 16 May 2014
ER -