{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T04:29:06Z","timestamp":1774672146049,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"unspecified","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":[[2017,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The main objective of this article is to present a complete finite black-box testing theory for non-deterministic Kripke structures with possibly infinite input domains, but finite domains for internal state variables and outputs. To this end, an abstraction from Kripke structures of this sub-domain to finite state machines is developed. It is shown that\n            <jats:italic>every<\/jats:italic>\n            complete black-box testing theory for (deterministic or nondeterministic) finite state machines in the range of this abstraction induces a complete black-box input equivalence class partition testing (IECPT) theory for the Kripke structures under consideration. Additionally, it is shown that each of these IECPT theories can be combined with random testing, such that a random value is selected from an input equivalence class, whenever a representative from this class is required in a test step. Experiments have shown that this combination increases the test strength of equivalence class tests for systems under test (SUT)\n            <jats:italic>outside<\/jats:italic>\n            the fault domain, while we show here that this randomisation preserves the completeness property for SUT\n            <jats:italic>inside<\/jats:italic>\n            the domain. The investigations lead to several complete IECPT strategies which, to our best knowledge, were not known before for this sub-domain of Kripke structures. The elaboration and presentation of results is performed on a semantic level, so that the testing theories under consideration can be applied to models presented in any concrete formalism, whose behaviour is reflected by a member of our semantic category.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0402-2","type":"journal-article","created":{"date-parts":[[2016,11,15]],"date-time":"2016-11-15T09:54:15Z","timestamp":1479203655000},"page":"335-364","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["Complete model-based equivalence class testing for nondeterministic systems"],"prefix":"10.1145","volume":"29","author":[{"given":"Wen-ling","family":"Huang","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3667-9775","authenticated-orcid":false,"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2013.02.061"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Braunstein C Haxthausen AE Huang W-L H\u00fcbner F Peleska J Schulze U Hong LV (2014) Complete model-based equivalence class testing for the ETCS ceiling speed monitor. In: Merz S Pang J (eds) Proceedings of the ICFEM 2014 Lecture Notes in Computer Science vol 8829. Springer Berlin Heidelberg pp 380\u2013395","DOI":"10.1007\/978-3-319-11737-9_25"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-011-0133-z"},{"key":"e_1_2_1_2_4_2","volume-title":"Model checking","author":"Clarke EM","year":"1999"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1978.231496"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti A Huang W-L Peleska J Woodcock J (2015) CSP and Kripke structures. In: Leucker M Rueda C Valencia FD (eds) Theoretical aspects of computing\u2013ICTAC 2015\u201412th International Colloquium Cali Colombia October 29\u201331 2015 Proceedings Lecture Notes in Computer Science vol 9399. Springer Switzerland pp 505\u2013523","DOI":"10.1007\/978-3-319-25150-9_29"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Dick J Faivre A (1993) Automating the generation and sequencing of test cases from model-based specifications. In: Woodcock JCP Larsen PG (eds) FME \u201993: industrial-strength formal methods Lecture Notes in Computer Science vol 670. Springer Berlin Heidelberg pp 268\u2013284","DOI":"10.1007\/BFb0024651"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/1481586"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.87284"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Frantzen L Tretmans J Willemse TAC (2005) Test generation based on symbolic specifications. In: Grabowski J Nielsen B (eds) Formal approaches to software testing Lecture Notes in Computer Science vol 3395. Springer Berlin Heidelberg pp 1\u201315","DOI":"10.1007\/978-3-540-31848-4_1"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Gaudel M-C (1995) Testing can be formal too. In: Mosses PD Nielsen M Schwartzbach MI (eds) TAPSOFT Lecture Notes in Computer Science vol 915. Springer Heidelberg pp 82\u201396","DOI":"10.1007\/3-540-59293-8_188"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/566171.566190"},{"issue":"3","key":"e_1_2_1_2_14_2","first-page":"274","article-title":"Institution morphisms","volume":"13","author":"Goguen J","year":"2014","journal-title":"Formal Aspects Comput"},{"key":"e_1_2_1_2_15_2","volume-title":"Algebraic theory of processes","author":"Hennessy M","year":"1988"},{"key":"e_1_2_1_2_16_2","unstructured":"H\u00fcbner F Huang W-L Peleska J (2015) Experimental evaluation of a novel equivalence class partition testing strategy. In: Christian Blanchette J Kosmatov N (eds) Tests and proofs\u20139th International Conference TAP 2015 Held as Part of STAF 2015 L\u2019Aquila Italy July 22\u201324 2015. Proceedings Lecture Notes in Computer Science vol 9154. Springer Switzerland pp 155\u2013172"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.85"},{"key":"e_1_2_1_2_18_2","volume-title":"Unifying theories of programming","author":"Hoare CAR","year":"1998"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Hong HS Lee I Sokolsky O Ural H (2002) A temporal logic based theory of test coverage and generation. In: Katoen J-P Stevens P (eds) TACAS Lecture Notes in Computer Science vol 2280. Springer Heidelberg pp 327\u2013341","DOI":"10.1007\/3-540-46002-0_23"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Helke S Neustupny T Santen T (1997) Automating test case generation from Z specifications with Isabelle. In: Bowen JP Hinchey MG Till D (eds) ZUM \u201997: The Z formal specification notation Lecture Notes in Computer Science vol 1212. Springer Berlin Heidelberg pp 52\u201371","DOI":"10.1007\/BFb0027283"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0356-8"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Kalaji AS Hierons RM Swift S (2009) Generating feasible transition paths for testing from an extended finite state machine (efsm). In: ICST. IEEE Computer Society New York pp 230\u2013239","DOI":"10.1109\/ICST.2009.29"},{"key":"e_1_2_1_2_23_2","unstructured":"Lapschies F (2014) SONOLAR homepage. http:\/\/www.informatik.uni-bremen.de\/agbs\/florian\/sonolar\/"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.265636"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Mossakowski T Roggenbach M (2006) Structured CSP\u2014a process algebra as an institution. In: Fiadeiro JL Schobbens P-Y (eds) Recent trends in algebraic development techniques 18th International Workshop WADT 2006 La Roche en Ardenne Belgium June 1\u20133 2006 Revised Selected Papers Lecture Notes in Computer Science vol 4409. Springer Heidelberg pp 92\u2013110","DOI":"10.1007\/978-3-540-71998-4_6"},{"key":"e_1_2_1_2_26_2","unstructured":"Naito S Tsunoyama M (1981) Fault detection for sequential machines by transition tours. In: Proc. IEEE Fault Tolerant Comput. Conf. pp 162\u2013178"},{"key":"e_1_2_1_2_27_2","unstructured":"Peleska J (1996) Formal Methods and the Development of Dependable Systems. Number 9612. Christian-Albrechts-Universit\u00e4t Kiel Institut fr Informatik und Praktische Mathematik Habilitationsschrift"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Peleska J (2013) Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko AK Schlingloff H (eds) Proceedings eighth workshop on model-based testing Rome Italy 17th March 2013 Electronic Proceedings in Theoretical Computer Science vol 111. Open Publishing Association Sydney pp 3\u201328","DOI":"10.4204\/EPTCS.111.1"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Peleska J Huang W-L H\u00fcbner F (2016) A novel approach to HW\/SW integration testing of route-based interlocking system controllers. In: Lecomte T Pinger R Romanovsky A (eds) Reliability safety and security of railway systems. modelling analysis verification and certification\u2013First International Conference RSSRail 2016 Paris France June 28\u201330 2016 Proceedings Lecture Notes in Computer Science vol 9707. Springer Switzerland pp 32\u201349","DOI":"10.1007\/978-3-319-33951-1_3"},{"key":"e_1_2_1_2_30_2","first-page":"53","article-title":"Test automation of safety-critical reactive systems","volume":"19","author":"Peleska J","year":"1997","journal-title":"S Afr Comput J"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxu113"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Peleska J Vorobev E Lapschies F (2011) Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru M Havelund K Holzmann GJ Joshi R (eds) Nasa formal methods Third International Symposium NFM 2011 LNCS vol 6617 Pasadena. Springer Heidelberg pp 298\u2013312","DOI":"10.1007\/978-3-642-20398-5_22"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Petrenko A Yevtushenko N (2011) Adaptive testing of deterministic implementations specified by nondeterministic FSMs. In: Testing software and systems Lecture Notes in Computer Science vol 7019. Springer Heidelberg pp 162\u2013178","DOI":"10.1007\/978-3-642-24580-0_12"},{"key":"e_1_2_1_2_34_2","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 New York pp 224\u2013228","DOI":"10.1109\/HASE.2014.39"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Petrenko A Yevtushenko N Bochmann GV (1996) Fault models for testing in context. In: Gotzhein R Bredereke J (eds) Formal description techniques IX\u2013Theory application and tools. Chapman & Hall London pp 163\u2013177","DOI":"10.1007\/978-0-387-35079-0_10"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Petrenko A Yevtushenko N Bochmann GV (1996) Testing deterministic implementations from nondeterministic FSM specifications. In: In testing of communicating systems IFIP TC6 9th International Workshop on Testing of Communicating Systems. Chapman and Hall London pp 125\u2013141","DOI":"10.1007\/978-0-387-35062-2_10"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_2_1_2_38_2","volume-title":"Abstract automata","author":"Starke PH","year":"1972"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00134-6"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0169-7552(96)00017-7"},{"key":"e_1_2_1_2_41_2","first-page":"98","article-title":"Failure diagnosis of automata","volume":"4","author":"Vasilevskii MP","year":"1973","journal-title":"Kibernetika (Transl.)"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Vu LH Haxthausen AE Peleska J (2015) Formal modeling and verification of interlocking systems featuring sequential release. In: Artho C \u00d6lveczky PC (eds) Formal techniques for safety-critical systems Communications in Computer and Information Science vol 476. Springer Switzerland pp 223\u2013238","DOI":"10.1007\/978-3-319-17581-2_15"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0402-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0402-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0402-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0402-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:56:37Z","timestamp":1641538597000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0402-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["10.1007\/s00165-016-0402-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0402-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3]]}}}