{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T01:10:01Z","timestamp":1748740201849,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"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,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In the last decade it became a common practice to formalise software requirements to improve the clarity of users\u2019 expectations. In this work we build on the fact that functional requirements can be expressed in temporal logic and we propose new sanity checking techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate approaches to consistency and redundancy checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). We further report on the experience obtained from employing the consistency and redundancy checking in an industrial environment. To complete the sanity checking we also describe a semi-automatic completeness evaluation that can assess the coverage of user requirements and suggest missing properties the user might have wanted to formulate. The usefulness of our completeness evaluation is demonstrated in a case study of an aeroplane control system.<\/jats:p>","DOI":"10.1007\/s00165-015-0348-9","type":"journal-article","created":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T11:47:28Z","timestamp":1451908048000},"page":"45-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Analysing sanity of requirements for avionics systems"],"prefix":"10.1145","volume":"28","author":[{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"first","affiliation":[{"name":"Faculty of Informatics, Masaryk University, Botanicka 68a, 602 00, Brno, Czech Republic"}]},{"given":"Petr","family":"Bauch","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, Masaryk University, Botanicka 68a, 602 00, Brno, Czech Republic"}]},{"given":"Nikola","family":"Bene\u0161","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, Masaryk University, Botanicka 68a, 602 00, Brno, Czech Republic"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, Masaryk University, Botanicka 68a, 602 00, Brno, Czech Republic"}]},{"given":"Jan","family":"Beran","sequence":"additional","affiliation":[{"name":"Honeywell International, Aerospace, Advanced Technology Europe, Brno, Czech Republic"}]},{"given":"Tom\u00e1\u0161","family":"Kratochv\u00edla","sequence":"additional","affiliation":[{"name":"Honeywell International, Aerospace, Advanced Technology Europe, Brno, Czech Republic"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abadi M Lamport L Wolper P (1989) Realizable and unrealizable specifications of reactive systems. In: Proceedings of ICALP pp 1\u201317","DOI":"10.1007\/BFb0035748"},{"key":"e_1_2_1_2_2_2","unstructured":"Bormann J Busch H (2009) Method for the determination of the quality of a set of properties usable for the verification and specification of circuits. U. S. Patent No. 7 571 398 B2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Barnat J Bauch P Brim L (2012) Checking sanity of software requirements. In: Proceedings of SEFM pp 48\u201352","DOI":"10.1007\/978-3-642-33826-7_4"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barnat J Beran J Brim L Kratochv\u00edla T Ro\u010dkai P (2012) Tool chain to support automated formal verification of avionics simulink designs. In: Proceedings of FMICS pp 78\u201392","DOI":"10.1007\/978-3-642-32469-7_6"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Barnat J Brim L \u010ce\u0161ka M Ro\u010dkai P (2010) DiVinE: parallel distributed model checker. In: Proceedings of HiBi\/PDMC pp 4\u20137","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008779610539"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bloem R Cimatti A Greimel K Hofferek G K\u00f6nighofer R Roveri M Schuppan V Seeber R (2010) RATSY\u2014a new requirements analysis tool with synthesis. In: Proceedings of CAV pp 425\u2013429","DOI":"10.1007\/978-3-642-14295-6_37"},{"key":"e_1_2_1_2_8_2","first-page":"250","volume-title":"CAV, vol 2102 of LNCS","author":"Blom S","year":"2001"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","article-title":"Model checking large software specifications","volume":"24","author":"Chan W","year":"1989","journal-title":"IEEE Trans. Softw Eng"},{"key":"e_1_2_1_2_10_2","first-page":"241","volume-title":"CAV, vol 2404 of LNCS","author":"Cimatti A","year":"2002"},{"key":"e_1_2_1_2_11_2","first-page":"66","volume-title":"CAV, vol 2102 of LNCS","author":"Chockler H","year":"2001"},{"key":"e_1_2_1_2_12_2","first-page":"528","volume-title":"TACAS, vol 2031 of LNCS","author":"Chockler H","year":"2001"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Roveri M Schuppan V Tchaltsev A (2008) Diagnostic information for realizability. In: Proceedings of VMCAI pp 52\u201367","DOI":"10.1007\/978-3-540-78163-9_9"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC (1998) Property specification patterns for finite-state verification. In: Proceedings of FMSP pp 7\u201315","DOI":"10.1145\/298595.298598"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A (2011) LTL translation improvements in spot. In: Proceedings of VECoS pp 72\u201383","DOI":"10.14236\/ewic\/VECOS2011.8"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Feierbach G Gupta V (2003) True coverage: a goal of verification. In: Proceedings of ISQED pp 75\u201378","DOI":"10.1109\/ISQED.2003.1194712"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1378727.1378742"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Heimdahl MPE Leveson NG (1995) Completeness and consistency analysis of state-based requirements. In: Proceedings of ICSE pp 3\u201314","DOI":"10.1145\/225014.225015"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Katz S Grumberg O Geist D (1999) \u201cHave I Written Enough Properties?\u201d\u2014a method of comparison between specification and implementation. In: Proceedings of CHARME pp 280\u2013297","DOI":"10.1007\/3-540-48153-2_21"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Konighofer R Hofferek G Bloem R (2009) Debugging formal specifications using simple counterstrategies. In: Proceedings of FMCAD pp 152\u2013159","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"e_1_2_1_2_22_2","first-page":"37","volume-title":"CONCUR, vol 4137 of LNCS","author":"Kupferman O","year":"2006"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Leveson N (2000) Completeness in formal specification language design for process-control systems. In: Proceedings of FMSP pp 75\u201387","DOI":"10.1145\/349360.351140"},{"key":"e_1_2_1_2_25_2","unstructured":"Lynce I Marques-Silva JP (2004) On computing minimum unsatisfiable cores. In: Proceedings of SAT pp 305\u2013310"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9084-z"},{"key":"e_1_2_1_2_27_2","first-page":"75","volume-title":"FME, vol 2805 of LNCS","author":"Miller SP","year":"2003"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Roy S Das S Basu P Dasgupta P Chakrabarti PP (2005) SAT based solutions for consistency problems in formal property specifications for open systems. In: Proceedings of ICCAD pp 885\u2013888","DOI":"10.1109\/ICCAD.2005.1560186"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Regimbal S Lemire J-F Savaria Y Bois G Aboulhamid E Baron A (2003) Automating functional coverage analysis based on an executable specification. In Proceedings of IWSOC pp 228\u2013234","DOI":"10.1109\/IWSOC.2003.1213040"},{"key":"e_1_2_1_2_30_2","first-page":"149","volume-title":"SPIN, vol 4595 of LNCS","author":"Rozier K","year":"2007"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Rajan A Whalen MW Heimdahl MPE (2007) Model validation using automatically generated requirements-based tests. In: Proceedings of HASE pp 95\u2013104","DOI":"10.1109\/HASE.2007.57"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.11.004"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/54.936247"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Whalen MW Rajan A Heimdahl MPE Miller SP (2006) Coverage metrics for requirements-based testing. In: Proceedings of ISSTA pp 25\u201336","DOI":"10.1145\/1146238.1146242"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0348-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0348-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0348-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:56:43Z","timestamp":1748739403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0348-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["10.1007\/s00165-015-0348-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0348-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,3]]}}}