TY - JOUR
T1 - Ready for testing
T2 - ensuring conformance to industrial standards through formal verification
AU - Feo-Arenis, Sergio
AU - Westphal, Bernd
AU - Dietsch, Daniel
AU - Muñiz, Marco
AU - Andisha, Siyar
AU - Podelski, Andreas
PY - 2016
Y1 - 2016
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 that stem from international standards. We present a case study that 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, regulated by the EN 54 standard. We performed formal requirements engineering, modeling and verification and uncovered severe design flaws that would have prevented its certification. For an improved design, we provided dependable verification results which in particular ensure that certification 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 those test procedures is a cost-efficient approach to improve the product quality based on formal methods. Based on our experience, we propose an approach useful to integrate the application of formal methods to product development in SME.
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 that stem from international standards. We present a case study that 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, regulated by the EN 54 standard. We performed formal requirements engineering, modeling and verification and uncovered severe design flaws that would have prevented its certification. For an improved design, we provided dependable verification results which in particular ensure that certification 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 those test procedures is a cost-efficient approach to improve the product quality based on formal methods. Based on our experience, we propose an approach useful to integrate the application of formal methods to product development in SME.
KW - Certification tests
KW - Dependability
KW - Model Checking
KW - Safety-critical systems
KW - SME
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=84960087056&partnerID=8YFLogxK
U2 - 10.1007/s00165-016-0365-3
DO - 10.1007/s00165-016-0365-3
M3 - Journal article
AN - SCOPUS:84960087056
SN - 0934-5043
VL - 28
SP - 499
EP - 527
JO - Formal Aspects of Computing
JF - Formal Aspects of Computing
IS - 3
ER -