{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,28]],"date-time":"2024-08-28T13:56:49Z","timestamp":1724853409992},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            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\n            <jats:italic>verifying<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0365-3","type":"journal-article","created":{"date-parts":[[2016,3,4]],"date-time":"2016-03-04T09:02:46Z","timestamp":1457082166000},"page":"499-527","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Ready for testing: ensuring conformance to industrial standards through formal verification"],"prefix":"10.1145","volume":"28","author":[{"given":"Sergio","family":"Feo-Arenis","sequence":"first","affiliation":[{"name":"Albert-Ludwigs Universit\u00e4t Freiburg, Georges-K\u00f6hler Allee 52, 79110, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Westphal","sequence":"additional","affiliation":[{"name":"Albert-Ludwigs Universit\u00e4t Freiburg, Georges-K\u00f6hler Allee 52, 79110, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Dietsch","sequence":"additional","affiliation":[{"name":"Albert-Ludwigs Universit\u00e4t Freiburg, Georges-K\u00f6hler Allee 52, 79110, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Mu\u00f1iz","sequence":"additional","affiliation":[{"name":"Aalborg University, Aalborg, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siyar","family":"Andisha","sequence":"additional","affiliation":[{"name":"Albert-Ludwigs Universit\u00e4t Freiburg, Georges-K\u00f6hler Allee 52, 79110, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"Albert-Ludwigs Universit\u00e4t Freiburg, Georges-K\u00f6hler Allee 52, 79110, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Aranda J Easterbrook SM Wilson G (2007) Requirements in the wild: how small companies do it. In: RE IEEE pp 39\u201348","DOI":"10.1109\/RE.2007.54"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Behrmann G David A Larsen KG (2004) A tutorial on Uppaal. In: SFM-RT 2004 number 3185 in LNCS Springer pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1166\/sl.2013.2653"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"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\u201377","DOI":"10.1007\/978-3-642-41010-9_5"},{"key":"e_1_2_1_2_8_2","unstructured":"Dietsch D Feo-Arenis S Westphal B (2010) Abwicklung von Sofwareentwicklungsauftr\u00e4gen in kleinen und mittleren Unternehmen: Analyse. Technical report Universities of Freiburg and Mannheim Project SALOMO"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"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\u2013270","DOI":"10.1109\/RE.2011.6051634"},{"key":"e_1_2_1_2_10_2","unstructured":"DIN eV (1997) Fire detection and fire alarm systems\u2014Part 2: Control and indicating equipment; German version EN 54-2"},{"key":"e_1_2_1_2_11_2","unstructured":"DIN eV (1997) Fire detection and fire alarm systems; German version EN 54"},{"key":"e_1_2_1_2_12_2","unstructured":"DIN eV (2005) Fire detection and fire alarm systems\u2014Part 25: Components using radio links and system requirements German version EN 54-25"},{"key":"e_1_2_1_2_13_2","unstructured":"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\u201999. Fifth IEEE international conference on IEEE pp 153\u2013160"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Fehnker A van Glabbeek RJ H\u00f6fner P McIver A Portmann M Tan WL (2012) Automated analysis of AODV using UPPAAL. In: Flanagan C K\u00f6nig B (eds) Tools and algorithms for the construction and analysis of systems\u201418th international conference TACAS volume 7214 of LNCS Springer pp 173\u2013187","DOI":"10.1007\/978-3-642-28756-5_13"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"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\u2013147","DOI":"10.1007\/978-3-642-15898-8_9"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019089616850"},{"key":"e_1_2_1_2_17_2","volume-title":"The RAISE Development Method. The BCS Practitioners Series","author":"George C","year":"1995"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","DOI":"10.1002\/9781118459898","volume-title":"Formal methods for industrial critical systems: a survey of applications","author":"Gnesi S","year":"2012"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"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\u201325 2006 Seoul Korea ACM pp 242\u2013251","DOI":"10.1145\/1176887.1176923"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.54292"},{"key":"e_1_2_1_2_21_2","volume-title":"The SPIN Model Checker\u2014primer and reference manual","author":"Holzmann GJ","year":"2004"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Halbwachs N Raymond P Ratel C (1991) Generating efficient code from data-flow programs. In: PLILP number 528 in LNCS Springer pp 207\u2013218","DOI":"10.1007\/3-540-54444-5_100"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Herrera C Westphal B Feo-Arenis S Mu\u00f1iz 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\u2013170","DOI":"10.1007\/978-3-642-33365-1_12"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Herrera C Westphal B Podelski A (2014) Quasi-equal clock reduction: more networks more queries. In: \u00c1brahams E Havelund K (eds) TACAS volume 8413 of Lecture Notes in Computer Science Springer pp 295\u2013309","DOI":"10.1007\/978-3-642-54862-8_20"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1498765.1498787"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Jubran O Westphal B (2013) Formal approach to guard time optimization for TDMA. In: RTNS ACM pp 223\u2013233","DOI":"10.1145\/2516821.2516849"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Jubran O Westphal B (2014) Optimizing guard time for TDMA in a wireless sensor network\u2014case study. In: LCN IEEE pp 597\u2013601","DOI":"10.1109\/LCNW.2014.6927708"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230854"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Kamali M (2010) Self-recovering sensor-actor networks. In: Mousavi MR Sala\u00fcn G (eds) FOCLASA volume 30 of EPTCS pp 47\u201361","DOI":"10.4204\/EPTCS.30.4"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805821"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"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\u00fa\u00f1ez M G\u00fcdemann M (eds) Formal methods for industrial critical systems (FMICS) 2015 volume 9128 of LNCS Springer pp 47\u201361","DOI":"10.1007\/978-3-319-19458-5_4"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-1494-9","volume-title":"The B Language and Method","author":"Lano K","year":"1996"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Laporte CY Alexandre S O\u2019Connor 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\u2013141","DOI":"10.1007\/978-3-540-85936-9_12"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-006-6883-y"},{"key":"e_1_2_1_2_35_2","volume-title":"Ad hoc wireless networks: architectures and protocols","author":"SivaRam Murthy C","year":"2004"},{"key":"e_1_2_1_2_36_2","unstructured":"Nokula U (2000) A state-of-the-practice survey on req. engineering in small- and medium-sized enterprises. Technical report Lappeenranta Univ. of Tech"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1241365"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.5555\/1453100"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020519822806"},{"key":"e_1_2_1_2_40_2","unstructured":"RTCA (2011) DO-333 Formal methods supplement to DO-178C and DO-278A"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.81"},{"key":"e_1_2_1_2_42_2","unstructured":"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\u201354"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Larsen PG Bicarregui J Fitzgerald J: (2009) Formal methods: practice and experience. ACM Comput Surv 41:19:1\u201319:36","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Wibling O Parrow J Pears AN (2004) Automatized verification of ad hoc routing protocols. In: de Frutos-Escrig D N\u00fa\u00f1ez M (eds) Formal techniques for networked and distributed systems (FORTE) volume 3235 of LNCS Springer pp 343\u2013358","DOI":"10.1007\/978-3-540-30232-2_22"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Wong-Toi H (1995) Symbolic approximations for verifying real-time systems. PhD thesis Stanford University","DOI":"10.1142\/9789812831583_0007"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0365-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0365-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0365-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:13:31Z","timestamp":1641485611000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0365-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["10.1007\/s00165-016-0365-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0365-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5]]}}}