{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T07:12:05Z","timestamp":1774681925408,"version":"3.50.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001834","name":"University of Twente","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001834","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This work presents an executable model-based testing framework for probabilistic systems with non-determinism. We provide algorithms to automatically generate, execute and evaluate test cases from a probabilistic requirements specification. The framework connects input\/output conformance-theory with hypothesis testing: our algorithms handle functional correctness, while statistical methods assess, if the frequencies observed during the test process correspond to the probabilities specified in the requirements. At the core of our work lies the conformance relation for probabilistic input\/output conformance, enabling us to pin down exactly when an implementation should pass a test case. We establish the correctness of our framework alongside this relation as soundness and completeness; Soundness states that a correct implementation indeed passes a test suite, while completeness states that the framework is powerful enough to discover each deviation from a specification up to arbitrary precision for a sufficiently large sample size. The underlying models are probabilistic automata that allow invisible internal progress. We incorporate divergent systems into our framework by phrasing four rules that each well-formed system needs to adhere to. This enables us to treat divergence as the absence of output, or quiescence, which is a well-studied formalism in model-based testing. Lastly, we illustrate the application of our framework on three case studies.<\/jats:p>","DOI":"10.1007\/s00165-017-0440-4","type":"journal-article","created":{"date-parts":[[2018,1,2]],"date-time":"2018-01-02T09:16:09Z","timestamp":1514884569000},"page":"77-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Model-based testing of probabilistic systems"],"prefix":"10.1145","volume":"30","author":[{"given":"Marcus","family":"Gerhold","sequence":"first","affiliation":[{"name":"Formal Methods and Tools Group, University of Twente, Enschede, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[{"name":"Formal Methods and Tools Group, University of Twente, Enschede, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1109\/MWC.2004.1368893"},{"key":"e_1_2_1_2_2_2","unstructured":"Briones LB Brinksma Ed (2004) A test generation framework for quiescent real-time systems. In: Proceedings of formal approaches to testing of software (4th international workshop) pp 71\u201385"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bohnenkamp H Belinfante A (2005) Timed testing with TorX. In: Formal methods Europe (FME) volume 3582 of LNCS pp 173\u2013188. Springer","DOI":"10.1007\/11526841_13"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129507006408"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Beyer M Dulz W (2005) Scenario-based statistical testing of quality of service requirements. In: Scenarios: models transformations and tools volume 3466 of LNCS pp 152\u2013173. Springer","DOI":"10.1007\/11495628_9"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bozga M David A Hartmanns A Hermanns H Larsen KG Legay A Tretmans J (2012) State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. In: DATE pp 370\u2013375","DOI":"10.1109\/DATE.2012.6176499"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Belinfante AEF (2010) JTorX: a tool for on-line model-driven test derivation and execution volume 6015 of LNCS pp 266\u2013270. Springer","DOI":"10.1007\/978-3-642-12002-2_21"},{"key":"e_1_2_1_2_8_2","volume-title":"Principles of model checking","author":"Baier C","year":"2008"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bernardo M De Nicola R Loreti M (2013) A uniform framework for modeling nondeterministic probabilistic stochastic or mixed processes and their behavioral equivalences. Inf Comput 225:29\u201382","DOI":"10.1016\/j.ic.2013.02.004"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"B\u00f6hr F (2011) Model based statistical testing of embedded systems. In: IEEE 4th international conference on software testing verification and validation workshops (ICSTW) pp 18\u201325","DOI":"10.1109\/ICSTW.2011.11"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Choi SG Dachman-Soled D Malkin T Wee H (2009) Improved non-committing encryption with applications to adaptively secure protocols. In: ASIACRYPT volume 5912 of LNCS pp 287\u2013302. Springer","DOI":"10.1007\/978-3-642-10366-7_17"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2808"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-0399-0","volume-title":"Measure Theory","author":"Cohn DL","year":"1980"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1314690.1314693"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Deng Y Hennessy M van Glabbeek RJ Morgan C (2008) Characterising testing preorders for finite probabilistic processes. CoRR","DOI":"10.2168\/LMCS-4(4:4)2008"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Desharnais J Laviolette F Tracol M (2008) Approximate analysis of probabilistic processes: logic simulation and games. In: 5th international conference on quantitative evaluation of systems pp 264\u2013273","DOI":"10.1109\/QEST.2008.42"},{"issue":"2","key":"e_1_2_1_2_17_2","first-page":"15","article-title":"An optimization of the torx test generation algorithm","volume":"8","author":"Goga N","year":"2000","journal-title":"Xootic Mag"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Gerhold M Stoelinga M (2015) Ioco theory for probabilistic automata. In: Proceedings of tenth workshop on MBT pp 23\u201340","DOI":"10.4204\/EPTCS.180.2"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Gerhold M Stoelinga M (2016) Model-based testing of probabilistic systems pp 251\u2013268. Springer Berlin","DOI":"10.1007\/978-3-662-49665-7_15"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Gerhold M Stoelinga M (2017) Model-based testing of probabilistic systems with stochastic time. In: Proceedings of the 11th international conference on tests and proofs TAP LNCS. Springer (to appear)","DOI":"10.1007\/978-3-319-61467-0_5"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"van Glabbeek RJ Smolka SA Steffen B Tofts CMN (1990) Reactive generative and stratified models of probabilistic processes pp 130\u2013141. IEEE Computer Society Press Philadelphia","DOI":"10.1109\/LICS.1990.113740"},{"key":"e_1_2_1_2_22_2","unstructured":"MATLAB Users Guide (1998) The Mathworks Inc. Natick MA vol 5 pp 333"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2009.10.014"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov chains: and the quest for quantified quality","author":"Hermanns H","year":"2002"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Hessel A Larsen KG Mikucionis M Nielsen B Pettersson P Skou A (2008) Testing real-time systems using UPPAAL volume 4949 of LNCS pp 77\u2013117. Springer","DOI":"10.1007\/978-3-540-78917-8_3"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.06.030"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hierons RM N\u00fa\u00f1ez M (2010) Testing probabilistic distributed systems volume 6117 of LNCS pp 63\u201377. Springer","DOI":"10.1007\/978-3-642-13464-7_6"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0244-5"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2017.03.011"},{"key":"e_1_2_1_2_30_2","unstructured":"Jeannet B D\u2019Argenio PR Larsen KG (2002) Rapture: a tool for verifying Markov decision processes. In: Tools day"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Jegourel C Legay A Sedwards S (2012) A platform for high performance statistical model checking\u2014PLASMA. Springer Heidelberg","DOI":"10.1007\/978-3-642-28756-5_37"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.256943"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2002) PRISM: probabilistic symbolic model checker. In: computer performance evaluation: modelling techniques and tools pp 200\u2013204. Springer","DOI":"10.1007\/3-540-46029-2_13"},{"key":"e_1_2_1_2_34_2","unstructured":"Knuth DE Yao AC (1976) The complexity of nonuniform random number generation. In: Traub JF (ed) Algorithms and complexity: new directions and recent results. Academic Press New York pp 357\u2013428"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Larsen KG Skou A (1989) Bisimulation through probabilistic testing pp 344\u2013352. ACM Press New York","DOI":"10.1145\/75277.75307"},{"key":"e_1_2_1_2_36_2","unstructured":"Marsan MA Balbo G Conte G Donatelli S Franceschinis G (1994) Modelling with generalized stochastic petri nets. Wiley Hoboken"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10898-006-9119-8"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Pfeffer A (2011) Practical probabilistic programming. In: Inductive logic programming volume 6489 of LNCS pp 2\u20133. Springer Berlin","DOI":"10.1007\/978-3-642-21295-6_2"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Peters H Knieke C Brox O Jauns-Seyfried S Kr\u00e4mer M Schulze A (2014) A test-driven approach for model-based development of powertrain functions. In: Agile processes in software engineering and extreme programming volume 179 of LNBIP pp 294\u2013301. Springer","DOI":"10.1007\/978-3-319-06862-6_23"},{"key":"e_1_2_1_2_42_2","unstructured":"Prowell SJ (2003) Computations for Markov chain usage models. Technical Report"},{"key":"e_1_2_1_2_43_2","volume-title":"Markov decision processes: discrete stochastic dynamic programming","author":"Puterman ML","year":"2014"},{"key":"e_1_2_1_2_44_2","unstructured":"Paige B Wood F (2014) A compilation target for probabilistic programming languages. CoRR arXiv:1403.0504"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Russell NJ Moore RK (1985) Explicit modelling of state occupancy in hidden markov models for automatic speech recognition. In: Acoustics speech and signal processing. IEEE international conference on ICASSP\u201985 volume 10 pp 5\u20138","DOI":"10.1109\/ICASSP.1985.1168477"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Remke A Stoelinga M (eds) (2014) Stochastic model checking. Rigorous dependability analysis using model checking techniques for stochastic systems\u2014International Autumn School ROCKS 2012 volume 8453 of LNCS. Springer","DOI":"10.1007\/978-3-662-45489-3"},{"key":"e_1_2_1_2_47_2","unstructured":"Segala R (1995) Modeling verification of randomized distributed real-time systems. Ph.D. thesis Cambridge MA USA"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Segala R (1996) Testing probabilistic automata. In: CONCUR 96: concurrency theory volume 1119 pp 299\u2013314. Springer","DOI":"10.1007\/3-540-61604-7_62"},{"key":"e_1_2_1_2_49_2","unstructured":"Stoelinga MIA (2002) Alea jacta est: verification of probabilistic real-time and parametric systems. Ph.D. thesis Radboud University of Nijmegen"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Stokkink WGJ Timmer M Stoelinga MIA (2013) Divergent quiescent transistion sytems. In: Proceedings 7th conference on tests and proofs (TAP\u201913) LNCS","DOI":"10.1007\/978-3-642-38916-0_13"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Stoelinga M Vaandrager F (1999) Root contention in IEEE 1394. In: Formal methods for real-time and probabilistic systems volume 1601 of LNCS pp 53\u201374. Springer Berlin","DOI":"10.1007\/3-540-48778-6_4"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Sen K Viswanathan M Agha G (2004) Statistical model checking of black-box probabilistic systems. In: Alur R Peled D (eds) 16th conference on computer aided verification (CAV) pp 202\u2013215","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Sen K Viswanathan M Agha G (2005) On statistical model checking of stochastic systems. In: CAV pp 266\u2013280","DOI":"10.1007\/11513988_26"},{"key":"e_1_2_1_2_54_2","volume-title":"Probabilistic robotics","author":"Thrun S","year":"2005"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Timmer M Brinksma H Stoelinga M (2011) Model-based testing. In: Software and systems safety: specification and verification volume 30 of NATO science for peace and security pp 1\u201332. IOS Press","DOI":"10.3233\/978-1-60750-711-6-1"},{"issue":"3","key":"e_1_2_1_2_56_2","first-page":"103","article-title":"Test generation with inputs, outputs and repetitive quiescence","volume":"17","author":"Tretmans J","year":"1996","journal-title":"Softw Concepts Tools"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Tretmans J (2008) Model based testing with labelled transition systems. In: Formal methods and testing volume 4949 of LNCS pp 1\u201338. Springer","DOI":"10.1007\/978-3-540-78917-8_1"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"van Osch M (2006) Hybrid input-output conformance and test generation. In: Proceeings of FATES\/RV 2006 number 4262 in LNCS pp 70\u201384","DOI":"10.1007\/11940197_5"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380250106"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00122-1"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0440-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0440-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0440-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0440-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,29]],"date-time":"2025-06-29T09:52:33Z","timestamp":1751190753000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0440-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1007\/s00165-017-0440-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0440-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1]]}}}