{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:11:20Z","timestamp":1750219880081,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100006668","name":"Fondo para la Investigaci\u00f3n Cient\u00edfica y Tecnol\u00f3gica","doi-asserted-by":"publisher","award":["PICT-2013-0080","PICT-2012-1298"],"award-info":[{"award-number":["PICT-2013-0080","PICT-2012-1298"]}],"id":[{"id":"10.13039\/501100006668","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a formal characterization of fault-tolerant behaviors of computing systems via simulation relations. This formalization makes use of variations of standard simulation relations in order to compare the executions of a system that exhibits faults with executions where no faults occur; intuitively, the latter can be understood as a specification of the system and the former as a fault-tolerant implementation. By employing variations of standard simulation algorithms, our characterization enables us to algorithmically check fault-tolerance in polynomial time, i.e., to verify that a system behaves in an acceptable way even subject to the occurrence of faults. Furthermore, the use of simulation relations in this setting allows us to distinguish between the different levels of fault-tolerance exhibited by systems during their execution. We prove that each kind of simulation relation preserves a corresponding class of temporal properties expressed in CTL; more precisely,<jats:italic>masking fault-tolerance<\/jats:italic>preserves liveness and safety properties,<jats:italic>nonmasking fault-tolerance<\/jats:italic>preserves liveness properties, while<jats:italic>failsafe fault-tolerance<\/jats:italic>guarantees the preservation of safety properties. We illustrate the suitability of this formal framework through its application to standard examples of fault-tolerance.<\/jats:p>","DOI":"10.1007\/s00165-017-0426-2","type":"journal-article","created":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T11:19:02Z","timestamp":1490354342000},"page":"1013-1050","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Simulation relations for fault-tolerance"],"prefix":"10.1145","volume":"29","author":[{"given":"Ramiro","family":"Demasi","sequence":"first","affiliation":[{"name":"Fondazione Bruno Kessler, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo F.","family":"Castro","sequence":"additional","affiliation":[{"name":"Departamento de Computaci\u00f3n, FCEFQyN, Universidad Nacional de R\u00edo Cuarto, Ruta Nac. No. 36 Km. 601, 5800, R\u00edo Cuarto, C\u00f3rdoba, Argentina"},{"name":"Consejo Nacional de Investigaciones Cient\u00edficas y T\u00e9cnicas (CONICET), Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas S. E.","family":"Maibaum","sequence":"additional","affiliation":[{"name":"Department of Computing and Software, McMaster University, Hamilton, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Departamento de Computaci\u00f3n, FCEFQyN, Universidad Nacional de R\u00edo Cuarto, Ruta Nac. No. 36 Km. 601, 5800, R\u00edo Cuarto, C\u00f3rdoba, Argentina"},{"name":"Consejo Nacional de Investigaciones Cient\u00edficas y T\u00e9cnicas (CONICET), Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/963778.963782"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abdelouahab Z Braga RI (2008) An adaptive train traffic controller. In: An adaptive train traffic controller. Springer Netherlands pp 550\u2013555","DOI":"10.1007\/978-1-4020-8735-6_102"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aminof B Ball T Kupferman O (2004) Reasoning about systems with transition fairness. In: Baader F Voronkov A (eds) Logic for programming artificial intelligence and reasoning 11th international conference LPAR 2004 volume 3452 of Lecture Notes in Computer Science pp 194\u2013208. Springer","DOI":"10.1007\/978-3-540-32275-7_14"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2006). Train systems. In: Butler MJ Jones CB Romanovsky A Troubitsynalena (eds) Rigorous development of complex fault-tolerant systems [FP6 IST-511599 RODIN project] RODIN Book volume 4157 of Lecture Notes in Computer Science pp 1\u201336. Springer","DOI":"10.1007\/11916246_1"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in event-B\u2014system and software engineering","author":"Abrial J-R","year":"2010"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.256850"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.663998"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Arora A Kulkarni SS (1998) Detectors and correctors: a theory of fault-tolerance components. In: 18th international conference on distributed computing systems ICDCS 1998 pp 436\u2013443. IEEE Computer Society","DOI":"10.1109\/ICDCS.1998.679772"},{"key":"e_1_2_1_2_9_2","unstructured":"Avizienis AA (1995) Software fault tolerance volume 2 chapter the methodology of N-version programming pp 22\u201345. Wiley"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Banach R Bozzano M (2006) Retrenchment and the generation of fault trees for static dynamic and cyclic systems. In: Computer safety reliability and security 25th international conference SAFECOMP 2006 Gdansk Poland 27\u201329 Sept 2006 Proceedings pp 127\u2013141","DOI":"10.1007\/11875567_10"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Banach R Cross R (2004) Safety requirements and fault trees using retrenchment. In: Computer safety reliability and security 23rd international conference SAFECOMP 2004 Potsdam Germany 21\u201324 Sept 2004 Proceedings pp 210\u2013223","DOI":"10.1007\/978-3-540-30138-7_18"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.258"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/48022.48023"},{"volume-title":"Principles of model checking","year":"2008","author":"Baier C","key":"e_1_2_1_2_14_2"},{"key":"e_1_2_1_2_15_2","unstructured":"Bonakdarpour B (2008) Automated revision of distributed and real-time programs. PhD thesis Michigan State University"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Banach R Poppleton M (1998) Retrenchment: an engineering variation on refinement. In: B\u201998: recent advances in the development and use of the B method second International B conference Montpellier France 22\u201324 April 1998 Proceedings pp 129\u2013147","DOI":"10.1007\/BFb0053358"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Banach R Poppleton M (1999) Retrenchment and punctured simulation. In: Integrated formal methods proceedings of the 1st international conference on integrated formal methods IFM 99 York UK 28\u201329 June 1999 pp 457\u2013476","DOI":"10.1007\/978-1-4471-0851-1_24"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.04.002"},{"key":"e_1_2_1_2_19_2","unstructured":"Braun B (2006) Implementing automatic addition and verification of fault tolerance. Master\u2019s thesis RWTH Aachen University"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Bradfield J Stirling C (2007) 12 modal mu-calculi. In: Van Benthem J Blackburn P Wolter F (eds) Handbook of modal logic volume 3 of studies in logic and practical reasoning pp 721\u2013756. Elsevier","DOI":"10.1016\/S1570-2464(07)80015-2"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Castro PF Kilmurray C Acosta A Aguirre N (2011) dCTL: a branching time temporal logic for fault-tolerant system verification. In: Barthe G Pardo A Schneider G (eds) Software engineering and formal methods\u20149th international conference SEFM 2011 volume 7041 of Lecture Notes in Computer Science pp 106\u2013121. Springer","DOI":"10.1007\/978-3-642-24690-6_9"},{"volume-title":"Model checking","year":"1999","author":"Clarke EM","key":"e_1_2_1_2_22_2"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Chandy KM Misra J (1989) Parallel program design\u2014a foundation. Addison-Wesley Reading","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.011"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231534"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Demasi R Castro PF Maibaum TSE Aguirre N (2013) Characterizing fault-tolerant systems by means of simulation relations. In: Johnsen EB Petre L (eds) Integrated formal methods 10th international conference IFM 2013 volume 7940 of Lecture Notes in Computer Science pp 428\u2013442. Springer","DOI":"10.1007\/978-3-642-38613-8_29"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Demasi R Castro PF Maibaum TSE Aguirre N (2013) Synthesizing masking fault-tolerant systems from deontic specifications. In: Van Hung D Ogawa M (eds) Automated technology for verification and analysis\u201411th international symposium ATVA 2013 volume 8172 of Lecture Notes in Computer Science pp 163\u2013177. Springer","DOI":"10.1007\/978-3-319-02444-8_13"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Demasi R Castro PF Ricci N Maibaum TSE Aguirre N (2015) syntmaskft: a tool for synthesizing masking fault-tolerant programs from deontic specifications. In: Tools and algorithms for the construction and analysis of systems\u201421st international conference TACAS 2015 Held as part of the European joint conferences on theory and practice of software ETAPS 2015 London UK 11\u201318 April 2015. Proceedings pp 188\u2013193","DOI":"10.1007\/978-3-662-46681-0_13"},{"volume-title":"A discipline of programming","year":"1976","author":"Dijkstra EW","key":"e_1_2_1_2_29_2"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Emerson EA Clarke EM (1980) Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker JW van Leeuwen J (eds) Automata languages and programming 7th colloquium ICALP 1980 volume 85 of Lecture Notes in Computer Science pp 169\u2013181. Springer","DOI":"10.1007\/3-540-10003-2_69"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_2_32_2","unstructured":"Ezekiel J Lomuscio A (2009) Combining fault injection and model checking to verify fault tolerance in multi-agent systems. In: Sierra C Castelfranchi C Decker KS Sichman JS (eds) 8th international joint conference on autonomous agents and multiagent systems AAMAS 2009 pp 113\u2013120. IFAAMAS"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.03.003"},{"key":"e_1_2_1_2_34_2","unstructured":"French T McCabe-Dansted JC Reynolds M (2007) A temporal logic of robustness. In: Frontiers of combining systems 6th international symposium FroCoS 2007 Liverpool UK 10\u201312 Sept 2007 Proceedings pp 193\u2013205"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/311531.311532"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Guiho GD Hennebert C (1990) SACEM software validation (experience report). In: Valette F-R Freeman PA Gaudel M-C (eds) Proceedings of the 12th international conference on software engineering ICSE 1990 pp 186\u2013191. IEEE Computer Society","DOI":"10.1109\/ICSE.1990.63621"},{"key":"e_1_2_1_2_37_2","unstructured":"Ghezzi C Jazayeri M Mandrioli D (2003) Fundamentals of software engineering 2nd edn. Prentice Hall Englewood Cliffs"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Henzinger MR Henzinger TA Kopke PW (1995) Computing simulations on finite and infinite graphs. In: 36th annual symposium on foundations of computer science FOCS 1995 pp 453\u2013462. IEEE Computer Society","DOI":"10.1109\/SFCS.1995.492576"},{"key":"e_1_2_1_2_39_2","unstructured":"Janowski T (1995) Bisimulation and fault-tolerance. PhD thesis University of Warwick United Kingdom"},{"key":"#cr-split#-e_1_2_1_2_40_2.1","doi-asserted-by":"crossref","unstructured":"Janowski T (1997) On bisimulation fault-monotonicity and provable fault-tolerance. In: Johnson M","DOI":"10.1007\/BFb0000478"},{"key":"#cr-split#-e_1_2_1_2_40_2.2","unstructured":"(ed) Algebraic methodology and software technology 6th international conference AMAST 1997 volume 1349 of Lecture Notes in Computer Science pp 292-306. Springer"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Jeffords RD Heitmeyer CL Archer M Leonard EI (2009) A formal method for developing provably correct fault-tolerant systems using partial refinement and composition. In: Cavalcanti A Dams D (eds) Formal methods second world congress FM 2009 volume 5850 of Lecture Notes in Computer Science pp 173\u2013189. Springer","DOI":"10.1007\/978-3-642-05089-3_12"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0106-9"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Lee PA Anderson T (1990) Fault tolerance: principles and practice 2nd edn. Springer Secaucus","DOI":"10.1007\/978-3-7091-8990-0"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/858336.858339"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"e_1_2_1_2_47_2","unstructured":"Mead C Conway L (1980) Introduction to VLSI systems. Addison-Wesley Reading"},{"key":"e_1_2_1_2_48_2","unstructured":"Milner R (1989) Communication and concurrency. PHI series in computer science. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_49_2","unstructured":"Manolios P Trefler RJ (2001) Safety and liveness in branching time. In: 16th annual IEEE symposium on logic in computer science Boston Massachusetts USA 16\u201319 June 2001 Proceedings pp 366\u2013374"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Rosner R (1989) On the synthesis of a reactive module. In: Sixteenth annual ACM symposium on principles of programming languages POPL 1989 pp 179\u2013190. ACM Press","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.5555\/1239380.1239385"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Schneider F Easterbrook SM Callahan JR Holzmann GJ (1998) Validating requirements for fault tolerant systems using model checking. In: 3rd international conference on requirements engineering ICRE 1998 pp 4\u201313. IEEE Computer Society","DOI":"10.1109\/ICRE.1998.667803"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Siewiorek DP Swarz RS (1998) Reliable computer systems 3rd edn: Design and evaluation. A. K. Peters Ltd. Natick","DOI":"10.1201\/9781439863961"},{"key":"e_1_2_1_2_54_2","unstructured":"Torres-Pomales W (2000) Software fault tolerance: a tutorial. Technical report NASA Technical Memorandum TM-2000-210616"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Yokogawa T Tsuchiya T Kikuno T (2001) Automatic verification of fault tolerance using model checking. In: 8th Pacific rim international symposium on dependable computing PRDC 2001 pp 95\u2013102. IEEE Computer Society","DOI":"10.1109\/PRDC.2001.992685"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0426-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0426-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0426-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0426-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:01:31Z","timestamp":1750179691000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0426-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":56,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["10.1007\/s00165-017-0426-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0426-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,11]]}}}