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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur R, Dill DL: (1994) A theory of timed automata. Theor Comput Sci 126(2), 183–235
Aranda J, Easterbrook SM, Wilson G (2007) Requirements in the wild: how small companies do it. In: RE, IEEE, pp 39–48
Behrmann G, David A, Larsen KG (2004) A tutorial on Uppaal. In: SFM-RT 2004, number 3185 in LNCS, Springer, pp 200–236
Bhargavan K, Obradovic D, Gunter CA: (2002) Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576
Chaochen Z, Richard Hoare CA, Ravn AP: (1991) A calculus of durations. Inf Process Lett 40(5), 269–276
Chen Z, Zhang D, Zhu R, Ma Y, Yin P, Xie F: (2013) A review of automated formal verification of ad hoc routing protocols for wireless sensor networks. Sensor Lett 11(5), 752–764
Davis JA, Clark MA, Cofer DD, Fifarek A, Hinchman J, Hoffman JA, Hulbert B, Miller SP, Wagner L (2013) Study on the barriers to the industrial adoption of formal methods. In: Pecheur C, Dierkes M (eds) Formal methods for industrial critical systems (FMICS) 2013, volume 8187 of LNCS, Springer, pp 63–77
Dietsch D, Feo-Arenis S, Westphal B (2010) Abwicklung von Sofwareentwicklungsaufträgen in kleinen und mittleren Unternehmen: Analyse. Technical report, Universities of Freiburg and Mannheim, Project SALOMO
Dietsch D, Feo-Arenis S, Westphal B, Podelski A (2011) Disambiguation of industrial standards through formalization and graphical languages. In: IEEE 19th international requirements engineering conference, pp 265–270
DIN eV (1997) Fire detection and fire alarm systems—Part 2: Control and indicating equipment; German version EN 54-2
DIN eV (1997) Fire detection and fire alarm systems; German version EN 54
DIN eV (2005) Fire detection and fire alarm systems—Part 25: Components using radio links and system requirements, German version EN 54-25
Dong Y, Smolka SA, Stark EW, White SM (1999) Practical considerations in protocol verification: the e-2c case study. In: Engineering of complex computer systems, 1999. ICECCS’99. Fifth IEEE international conference on, IEEE, pp 153–160
Fehnker A, van Glabbeek RJ, Höfner P, McIver A, Portmann M, Tan WL (2012) Automated analysis of AODV using UPPAAL. In: Flanagan C, König B (eds) Tools and algorithms for the construction and analysis of systems—18th international conference, TACAS, volume 7214 of LNCS, Springer, pp 173–187
Gerke M, Ehlers R, Finkbeiner B, Peter H (2010) Model checking the flexray physical layer protocol. In: Kowalewski S, Roveri M (eds) Formal methods for industrial critical systems - 15th international workshop, FMICS, volume 6371 of LNCS, Springer, pp 132–147
Garcés R, Garcia-Luna-Aceves JJ: (1998) Collision avoidance and resolution multiple access (CARMA). Clust Comput 1(2), 197–212
George C, Haxthausen AE: (1995) The RAISE Development Method. The BCS Practitioners Series. Prentice Hall Int, UK
Gnesi S, Margaria T: (2012) Formal methods for industrial critical systems: a survey of applications. Wiley, New York
Gebremichael B, Vaandrager FW, Zhang M (2006) Analysis of the zeroconf protocol using UPPAAL. In: Sang Lyul M, Wang Y (eds) Proceedings of the 6th ACM and IEEE International conference on Embedded software, EMSOFT 2006, October 22–25, 2006, Seoul, Korea, ACM, pp 242–251
Harel D, Lachover H, Naamad A, Pnueli A, Politi M, Sherman R, Shtull-Trauring A, Trakhtenbrot MB: (1990) STATEMATE: A working environment for the development of complex reactive systems. IEEE Trans Software Eng 16(4), 403–414
Holzmann GJ: (2004) The SPIN Model Checker—primer and reference manual. Addison-Wesley, USA
Halbwachs N, Raymond P, Ratel C (1991) Generating efficient code from data-flow programs. In: PLILP, number 528 in LNCS, Springer, pp 207–218
Herrera C, Westphal B, Feo-Arenis S, Muñiz M, Podelski A (2012) Reducing quasi-equal clocks in networks of timed automata. In: Jurdzinski M, Nickovic D (eds) FORMATS, volume 7595 of Lecture notes in computer science, Springer, pp 155–170
Herrera C, Westphal B, Podelski A (2014) Quasi-equal clock reduction: more networks, more queries. In: Ábrahams E, Havelund K, (eds) TACAS, volume 8413 of Lecture Notes in Computer Science, Springer, pp 295–309
Jackson D: (2009) A direct path to dependable software. CACM 52(4), 78–88
Jubran O, Westphal B (2013) Formal approach to guard time optimization for TDMA. In: RTNS, ACM, pp 223–233
Jubran O, Westphal B (2014) Optimizing guard time for TDMA in a wireless sensor network—case study. In: LCN, IEEE, pp 597–601
Kant E: (1981) The refinement paradigm: the interaction of coding and efficiency knowledge in program synthesis. IEEE Trans. Softw Eng 7(5), 458–471
Kamali M (2010) Self-recovering sensor-actor networks. In: Mousavi MR, Salaün G (eds) FOCLASA, volume 30 of EPTCS, pp 47–61
Kopetz H, Bauer G: (2003) The time-triggered architecture. Proc IEEE 91(1), 112–126
Kim JH, Larsen KG, Nielsen B, Mikucionis M, Olsen P (2015) Formal analysis and testing of real-time automotive systems using UPPAAL tools. In: Núñez M, Güdemann M (eds) Formal methods for industrial critical systems (FMICS) 2015, volume 9128 of LNCS, Springer, pp 47–61
Lano K: (1996) The B Language and Method. Springer, New York
Laporte CY, Alexandre S, O’Connor R (2008) A software engineering lifecycle standard for very small enterprises. In: Software process improvement, 15th European Conference, EuroSPI, volume 16 of communications in computer and information science, Springer, pp 129–141
Madl G, Abdelwahed S, Schmidt DC: (2006) Verifying distributed real-time properties of embedded systems via graph transformations and model checking. Real-Time Syst 33(1-3), 77–100
SivaRam Murthy C, Manoj BS: (2004) Ad hoc wireless networks: architectures and protocols. Prentice Hall PTR, UK
Nokula U (2000) A state-of-the-practice survey on req. engineering in small- and medium-sized enterprises. Technical report, Lappeenranta Univ. of Tech
Neill CJ, Laplante PA: (2003) Requirements engineering: the state of the practice. IEEE Softw 20(6), 40–45
Olderog E-R, Dierks H: (2008) Real-time systems. Cambridge University Press, Cambridge
Richardson I: (2002) SPI models: what characteristics are required for small software development companies?. Softw Quality J 10(2), 101–114
RTCA (2011) DO-333 Formal methods supplement to DO-178C and DO-278A
Tripakis S, Pinello C, Benveniste A, Sangiovanni-Vincentelli AL, Caspi P, Natale MD: (2008) Implementing synchronous models on loosely time triggered architectures. IEEE Trans Comput 57(10), 1300–1314
van Osch MJP, Smolka SA (2001) Finite-state analysis of the CAN bus protocol. In: 6th IEEE international symposium on high-assurance systems engineering (HASE 2001), Special topic: impact of networking, IEEE Computer Society, pp 42–54
Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J: (2009) Formal methods: practice and experience. ACM Comput Surv 41:19:1–19:36
Wibling O, Parrow J, Pears AN (2004) Automatized verification of ad hoc routing protocols. In: de Frutos-Escrig D, Núñez M (eds) Formal techniques for networked and distributed systems (FORTE), volume 3235 of LNCS, Springer, pp 343–358
Wong-Toi H (1995) Symbolic approximations for verifying real-time systems. PhD thesis, Stanford University
Author information
Authors and Affiliations
Corresponding author
Additional information
Stephan Merz, Jun Pang, and Jin Song Dong
Rights and permissions
About this article
Cite this article
Feo-Arenis, S., Westphal, B., Dietsch, D. et al. Ready for testing: ensuring conformance to industrial standards through formal verification. Form Asp Comp 28, 499–527 (2016). https://doi.org/10.1007/s00165-016-0365-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0365-3