{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:54:03Z","timestamp":1764053643301,"version":"3.37.3"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,10,14]],"date-time":"2019-10-14T00:00:00Z","timestamp":1571011200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,10,14]],"date-time":"2019-10-14T00:00:00Z","timestamp":1571011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020","doi-asserted-by":"publisher","award":["644905"],"award-info":[{"award-number":["644905"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11406-N23"],"award-info":[{"award-number":["S11406-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults in<jats:italic>every<\/jats:italic>realization of the specification and for<jats:italic>every<\/jats:italic>behavior of the uncontrollable part of the system\u2019s environment. The proposed approach supports different assumptions on occurrences of faults (ranging from a single transient fault to a persistent fault) and by default aims at unveiling the weakest one. We argue that such tests are also sensitive for more complex bugs. Since the specification may not define the system behavior completely, we use reactive synthesis algorithms with partial information. The computed strategies are<jats:italic>adaptive test strategies<\/jats:italic>that react to behavior at runtime. We work out the underlying theory of adaptive test strategy synthesis and present experiments for a safety-critical component of a real-world satellite system. We demonstrate that our approach can be applied to industrial specifications and that the synthesized test strategies are capable of detecting bugs that are hard to detect with random testing.<\/jats:p>","DOI":"10.1007\/s10703-019-00338-9","type":"journal-article","created":{"date-parts":[[2019,10,14]],"date-time":"2019-10-14T12:04:19Z","timestamp":1571054659000},"page":"103-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Synthesizing adaptive test strategies from temporal logic specifications"],"prefix":"10.1007","volume":"55","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Goerschwin","family":"Fey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabian","family":"Greif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"K\u00f6nighofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ingo","family":"Pill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heinz","family":"Riener","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7432-1419","authenticated-orcid":false,"given":"Franz","family":"R\u00f6ck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,14]]},"reference":[{"key":"338_CR1","doi-asserted-by":"crossref","unstructured":"Acree AT, Budd TA, DeMillo RA, Lipton RJ, Sayward FG (1979) Mutation analysis. Technical report GIT-ICS-79\/08, Georgia Institute of Technology, Atlanta, Georgia","DOI":"10.21236\/ADA076575"},{"issue":"8","key":"338_CR2","doi-asserted-by":"publisher","first-page":"716","DOI":"10.1002\/stvr.1522","volume":"25","author":"BK Aichernig","year":"2015","unstructured":"Aichernig BK, Brandl H, J\u00f6bstl E, Krenn W, Schlick R (2015) Killing strategies for model-based mutation testing. Softw Test Verif Reliab 25(8):716\u2013748","journal-title":"Softw Test Verif Reliab"},{"key":"338_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Yannakakis M (1995) Distinguishing tests for nondeterministic and probabilistic machines. In: Leighton FT, Borodin A (eds) Proceedings of the twenty-seventh annual ACM symposium on theory of computing, 29 May\u20131 June 1995, Las Vegas, Nevada, USA. ACM, pp 363\u2013372","DOI":"10.1145\/225058.225161"},{"key":"338_CR4","doi-asserted-by":"crossref","unstructured":"Ammann P, Ding W, Xu D (2001) Using a model checker to test safety properties. In: 7th International conference on engineering of complex computer systems (ICECCS 2001), 11\u201313 June 2001. Sweden. IEEE Computer Society, Sk\u00f6vde, pp 212\u2013221","DOI":"10.1109\/ICECCS.2001.930180"},{"key":"338_CR5","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Computer Aided Verification","author":"Roy Armoni","year":"2003","unstructured":"Armoni R, Fix L, Flaisher A, Grumberg O, Piterman N, Tiemeyer A, Vardi MY (2003) Enhanced vacuity detection in linear temporal logic. In: Hunt WA Jr, Somenzi F (eds) Proceedings of the 15th international conference on computer aided verification, CAV 2003, Boulder, CO, USA, 8\u201312 July 2003, volume 2725 of lecture notes in computer science. Springer, Berlin, pp 368\u2013380"},{"issue":"4","key":"338_CR6","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14:1\u201314:64","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"2","key":"338_CR7","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer I, Ben-David S, Eisner C, Rodeh Y (2001) Efficient detection of vacuity in temporal model checking. Formal Methods Syst Des 18(2):141\u2013163","journal-title":"Formal Methods Syst Des"},{"key":"338_CR8","doi-asserted-by":"crossref","unstructured":"Blass A, Gurevich Y, Nachmanson L, Veanes M Play to test. In: Grieskamp and Weise [26], pp 32\u201346","DOI":"10.1007\/11759744_3"},{"key":"338_CR9","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1007\/978-3-319-10575-8_27","volume-title":"Handbook of model checking","author":"R Bloem","year":"2018","unstructured":"Bloem R, Chatterjee K, Jobstmann B (2018) Graph games and reactive synthesis. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of model checking. Springer, Berlin, pp 921\u2013962"},{"key":"338_CR10","doi-asserted-by":"crossref","unstructured":"Bloem R, K\u00f6nighofer R, Pill I, R\u00f6ck F (2016) Synthesizing adaptive test strategies from temporal logic specifications. In: Piskac R, Talupur M (eds) 2016 Formal methods in computer-aided design, FMCAD 2016, Mountain View, CA, USA, 3\u20136 Oct 2016. IEEE, pp 17\u201324","DOI":"10.1109\/FMCAD.2016.7886656"},{"issue":"2","key":"338_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.08.002","volume":"190","author":"S Boroday","year":"2007","unstructured":"Boroday S, Petrenko A, Groz R (2007) Can a model checker generate tests for non-deterministic systems? Electr Notes Theor Comput Sci 190(2):3\u201319","journal-title":"Electr Notes Theor Comput Sci"},{"key":"338_CR12","first-page":"52","volume-title":"Logics of programs, workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of lecture notes in computer science","author":"EM Clarke","year":"1981","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen D (ed) Logics of programs, workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of lecture notes in computer science. Springer, Berlin, pp 52\u201371"},{"key":"#cr-split#-338_CR13.1","doi-asserted-by":"crossref","unstructured":"David A, Larsen KG, Li S, Nielsen B (2008) A game-theoretic approach to real-time system testing. In: Sciuto D","DOI":"10.1109\/DATE.2008.4484728"},{"key":"#cr-split#-338_CR13.2","unstructured":"(ed) Design, automation and test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008. ACM, pp 486-491"},{"key":"338_CR14","doi-asserted-by":"crossref","unstructured":"De Giacomo G, De Masellis R, Montali M (2014) Reasoning on LTL on finite traces: Insensitivity to infiniteness. In: Brodley CE, Stone P (eds) Proceedings of the twenty-eighth AAAI conference on artificial intelligence, July 27\u201331, 2014, Qu\u00e9bec City, Qu\u00e9bec, Canada. AAAI Press, pp 1027\u20131033","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"#cr-split#-338_CR15.1","unstructured":"De Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Rossi F"},{"key":"#cr-split#-338_CR15.2","unstructured":"(ed) IJCAI 2013, Proceedings of the 23rd international joint conference on artificial intelligence, Beijing, China, August 3-9, 2013. IJCAI\/AAAI, pp 854-860"},{"issue":"4","key":"338_CR16","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/C-M.1978.218136","volume":"11","author":"RA DeMillo","year":"1978","unstructured":"DeMillo RA, Lipton RJ, Sayward FG (1978) Hints on test data selection: help for the practicing programmer. IEEE Comput 11(4):34\u201341","journal-title":"IEEE Comput"},{"key":"338_CR17","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-31424-7_30","volume-title":"Computer Aided Verification","author":"Isil Dillig","year":"2012","unstructured":"Dillig I, Dillig T, McMillan KL, Aiken A (2012) Minimum satisfying assignments for SMT. In: Madhusudan P, Seshia SA (eds) Proceedings of the 24th international conference on computer aided verification\u2014CAV 2012, Berkeley, CA, USA, July 7\u201313, 2012, volume 7358 of lecture notes in computer science. Springer, pp. 394\u2013409"},{"issue":"2","key":"338_CR18","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/s10703-011-0137-x","volume":"40","author":"R Ehlers","year":"2012","unstructured":"Ehlers R (2012) Symbolic bounded synthesis. Form Methods Syst Des 40(2):232\u2013262","journal-title":"Form Methods Syst Des"},{"key":"338_CR19","unstructured":"Faella M (2008) Best-effort strategies for losing states. CoRR arXiv:0811.1664"},{"key":"#cr-split#-338_CR20.1","doi-asserted-by":"crossref","unstructured":"Faella M (2009) Admissible strategies in infinite games over graphs. In: Kr\u00e1lovic R, Niwinski D","DOI":"10.1007\/978-3-642-03816-7_27"},{"key":"#cr-split#-338_CR20.2","unstructured":"(ed) Proceedings of the 34th international symposium on mathematical foundations of computer science 2009, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Volume 5734 of lecture notes in computer science. Springer, pp 307-318"},{"issue":"5\u20136","key":"338_CR21","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner B, Schewe S (2013) Bounded synthesis. STTT 15(5\u20136):519\u2013539","journal-title":"STTT"},{"key":"#cr-split#-338_CR22.1","doi-asserted-by":"crossref","unstructured":"Fraser G, Ammann P (2008) Reachability and propagation for LTL requirements testing. In: Zhu H","DOI":"10.1109\/QSIC.2008.21"},{"key":"#cr-split#-338_CR22.2","unstructured":"(ed) Proceedings of the eighth international conference on quality software, QSIC 2008, 12-13 August 2008, Oxford, UK. IEEE Computer Society, pp 189-198"},{"key":"338_CR23","doi-asserted-by":"crossref","unstructured":"Fraser G, Wotawa F (2007) Test-case generation and coverage analysis for nondeterministic systems using model-checkers. In: Proceedings of the second international conference on software engineering advances (ICSEA 2007), August 25\u201331, 2007, Cap Esterel, French Riviera, France. IEEE Computer Society, p 45","DOI":"10.1109\/ICSEA.2007.71"},{"issue":"9","key":"338_CR24","doi-asserted-by":"publisher","first-page":"1403","DOI":"10.1016\/j.jss.2009.05.016","volume":"82","author":"G Fraser","year":"2009","unstructured":"Fraser G, Wotawa F, Ammann P (2009) Issues in using model checkers for test case generation. J Syst Softw 82(9):1403\u20131418","journal-title":"J Syst Softw"},{"issue":"3","key":"338_CR25","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1002\/stvr.402","volume":"19","author":"G Fraser","year":"2009","unstructured":"Fraser G, Wotawa F, Ammann P (2009) Testing with model checkers: a survey. Softw Test Verif Reliab 19(3):215\u2013261","journal-title":"Softw Test Verif Reliab"},{"key":"338_CR26","unstructured":"Grieskamp W, Weise C (eds) (2006) Formal approaches to software testing, 5th international workshop, FATES 2005, Edinburgh, UK, July 11, 2005, revised selected papers, vol 3997. Lecture notes in computer science. Springer"},{"key":"338_CR27","doi-asserted-by":"crossref","unstructured":"Havelund K, Rosu G (2001) Monitoring programs using rewriting. In: 16th IEEE international conference on automated software engineering (ASE 2001), 26\u201329 November 2001, Coronado Island, San Diego, CA, USA. IEEE Computer Society, pp 135\u2013143","DOI":"10.1109\/ASE.2001.989799"},{"issue":"2","key":"338_CR28","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.ipl.2005.12.001","volume":"98","author":"RM Hierons","year":"2006","unstructured":"Hierons RM (2006) Applying adaptive test cases to nondeterministic implementations. Inf Process Lett 98(2):56\u201360","journal-title":"Inf Process Lett"},{"issue":"5","key":"338_CR29","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia Y, Harman M (2011) An analysis and survey of the development of mutation testing. IEEE Trans Softw Eng 37(5):649\u2013678","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"338_CR30","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/s10009-004-0146-9","volume":"6","author":"HS Jin","year":"2004","unstructured":"Jin HS, Ravi K, Somenzi F (2004) Fate and free will in error traces. STTT 6(2):102\u2013116","journal-title":"STTT"},{"key":"338_CR31","doi-asserted-by":"crossref","unstructured":"Khalimov A, Jacobs S, Bloem R (2013) PARTY parameterized synthesis of token rings. In: Sharygina N, Veith H (eds) Proceedings of the 25th international conference on computer aided verification\u2014CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Volume 8044 of lecture notes in computer science. Springer, pp 928\u2013933","DOI":"10.1007\/978-3-642-39799-8_66"},{"issue":"5\u20136","key":"338_CR32","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/s10009-011-0221-y","volume":"15","author":"R K\u00f6nighofer","year":"2013","unstructured":"K\u00f6nighofer R, Hofferek G, Bloem R (2013) Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. STTT 15(5\u20136):563\u2013583","journal-title":"STTT"},{"key":"338_CR33","first-page":"109","volume-title":"Applied Logic Series","author":"Orna Kupfermant","year":"2000","unstructured":"Kupfermant O, Vardit MY (2000) Synthesis with incomplete information. In: Barringer H, Fisher M, Gabbay D, Gough G (eds) Advances in temporal logic. Applied Logic Series, vol 16. Springer, Dordrecht"},{"issue":"2","key":"338_CR34","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman O, Vardi MY (2003) Vacuity detection in temporal model checking. STTT 4(2):224\u2013233","journal-title":"STTT"},{"issue":"2","key":"338_CR35","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1109\/32.265636","volume":"20","author":"G Luo","year":"1994","unstructured":"Luo G, von Bochmann G, Petrenko A (1994) Test selection based on communicating nondeterministic finite-state machines using a generalized wp-method. IEEE Trans Softw Eng 20(2):149\u2013162","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"338_CR36","doi-asserted-by":"publisher","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"DA Martin","year":"1975","unstructured":"Martin DA (1975) Borel determinacy. Ann Math 102(2):363\u2013371","journal-title":"Ann Math"},{"key":"338_CR37","volume-title":"Foundations of software testing","author":"AP Mathur","year":"2008","unstructured":"Mathur AP (2008) Foundations of software testing, 2nd edn. Addison-Wesley, Boston","edition":"2"},{"issue":"2","key":"338_CR38","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1109\/TCAD.2003.822103","volume":"23","author":"K Miyase","year":"2004","unstructured":"Miyase K, Kajihara S (2004) XID: don\u2019t care identification of test patterns for combinational circuits. IEEE Trans CAD Integr Circuits Syst 23(2):321\u2013326","journal-title":"IEEE Trans CAD Integr Circuits Syst"},{"key":"338_CR39","doi-asserted-by":"crossref","unstructured":"Morgenstern A, Gesell M, Schneider K (2012) An asymptotically correct finite path semantics for LTL. In: Bj\u00f8rner N, Voronkov A (eds) Proceedings of the 18th international conference on logic for programming, artificial intelligence, and reasoning, LPAR-18, M\u00e9rida, Venezuela, March 11\u201315, 2012. Volume 7180 of lecture notes in computer science. Springer, pp 304\u2013319","DOI":"10.1007\/978-3-642-28717-6_24"},{"key":"338_CR40","doi-asserted-by":"crossref","unstructured":"Nachmanson L, Veanes M, Schulte W, Tillmann N, Grieskamp W (2004) Optimal strategies for testing nondeterministic systems. In: Avrunin GS, Rothermel G (eds) Proceedings of the ACM\/SIGSOFT international symposium on software testing and analysis, ISSTA 2004, Boston, MA, USA, July 11\u201314, 2004. ACM, pp 55\u201364","DOI":"10.1145\/1007512.1007520"},{"issue":"1","key":"338_CR41","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/125489.125473","volume":"1","author":"AJ Offutt","year":"1992","unstructured":"Offutt AJ (1992) Investigations of the software testing coupling effect. ACM Trans Softw Eng Methodol 1(1):5\u201320","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"338_CR42","doi-asserted-by":"crossref","unstructured":"Petrenko A, da Silva Sim\u00e3o A, Yevtushenko N (2012) Generating checking sequences for nondeterministic finite state machines. In: Antoniol G, Bertolino A, Labiche Y (eds) Fifth IEEE international conference on software testing, verification and validation, ICST 2012, Montreal, QC, Canada, April 17\u201321, 2012. IEEE Computer Society, pp 310\u2013319","DOI":"10.1109\/ICST.2012.111"},{"issue":"7","key":"338_CR43","doi-asserted-by":"publisher","first-page":"1656","DOI":"10.1093\/comjnl\/bxu113","volume":"58","author":"A Petrenko","year":"2015","unstructured":"Petrenko A, Sim\u00e3o A (2015) Generalizing the ds-methods for testing non-deterministic fsms. Comput J 58(7):1656\u20131672","journal-title":"Comput J"},{"key":"338_CR44","doi-asserted-by":"crossref","unstructured":"Petrenko A, Yevtushenko N. Conformance tests as checking experiments for partial nondeterministic FSM. In: Grieskamp and Weise [26], pp 118\u2013133","DOI":"10.1007\/11759744_9"},{"key":"338_CR45","doi-asserted-by":"crossref","unstructured":"Petrenko A, Yevtushenko N (2014) Adaptive testing of nondeterministic systems with FSM. In: 15th international IEEE symposium on high-assurance systems engineering, HASE 2014, Miami Beach, FL, USA, January 9\u201311, 2014. IEEE Computer Society, pp 224\u2013228","DOI":"10.1109\/HASE.2014.39"},{"key":"338_CR46","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, Rhode Island, USA, 31 October\u20131 November 1977. IEEE Computer Society, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"338_CR47","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Conference record of the sixteenth annual ACM symposium on principles of programming languages, Austin, Texas, USA, January 11\u201313, 1989. ACM Press, pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"338_CR48","first-page":"337","volume-title":"Lecture Notes in Computer Science","author":"J. P. Queille","year":"1982","unstructured":"Queille J-P, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini M, Montanari U (eds) Proceedings of the international symposium on programming, 5th colloquium, Torino, Italy, April 6\u20138, 1982, volume 137 of lecture notes in computer science. Springer, pp 337\u2013351"},{"issue":"1","key":"338_CR49","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0169-7552(96)00017-7","volume":"29","author":"J Tretmans","year":"1996","unstructured":"Tretmans J (1996) Conformance testing with labelled transition systems: implementation relations and test generation. Comput Netw ISDN Syst 29(1):49\u201379","journal-title":"Comput Netw ISDN Syst"},{"key":"338_CR50","unstructured":"Tan L, Sokolsky O, Lee I (2004) Specification-based testing with linear temporal logic. In: Zhang D, Gr\u00e9goire \u00c9, DeGroot D (eds) Proceedings of the 2004 IEEE international conference on information reuse and integration, IRI\u20142004, November 8\u201310, 2004, Las Vegas Hilton, Las Vegas, NV, USA. IEEE Systems, Man, and Cybernetics Society, pp 493\u2013498"},{"issue":"2","key":"338_CR51","first-page":"235","volume":"12","author":"M Tipaldi","year":"2015","unstructured":"Tipaldi M, Bruenjes B (2015) Survey on fault detection, isolation, and recovery strategies in the space domain. J Aerosp Inf Syst 12(2):235\u2013256","journal-title":"J Aerosp Inf Syst"},{"key":"338_CR52","doi-asserted-by":"crossref","unstructured":"Yannakakis M (2004) Testing, optimizaton, and games. In: D\u00edaz J, Karhum\u00e4ki J, Lepist\u00f6 A, Sannella D (eds) Proceedings of the automata, languages and programming: 31st international colloquium, ICALP 2004, Turku, Finland, July 12\u201316, 2004. Volume 3142 of lecture notes in computer science. Springer, pp 28\u201345","DOI":"10.1007\/978-3-540-27836-8_6"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00338-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00338-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00338-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T18:34:47Z","timestamp":1664649287000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00338-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,14]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["338"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00338-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2019,10,14]]},"assertion":[{"value":"14 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}