Title
Ready for testing: ensuring conformance to industrial standards through formal verification.
Abstract
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.
Year
DOI
Venue
2016
10.1007/s00165-016-0365-3
Formal Asp. Comput.
Keywords
Field
DocType
Certification tests, Verification, Model Checking, SME, Dependability, Safety-critical systems
Functional verification,Life-critical system,Software engineering,Computer science,Computer security,Theoretical computer science,Verification,Runtime verification,Formal methods,Certification,Formal verification,New product development
Journal
Volume
Issue
ISSN
28
3
1433-299X
Citations 
PageRank 
References 
2
0.49
33
Authors
6
Name
Order
Citations
PageRank
Sergio Feo-Arenis1214.00
Bernd Westphal2438.45
Daniel Dietsch38013.53
Marco Muñiz4545.68
Ahmad Siyar Andisha581.36
Andreas Podelski62760197.87