Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Al-Karaki JN, Kamal AE (2004) Routing techniques in wireless sensor networks: a survey. IEEE Wirel Commun 11(6): 6–28
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–85
Bohnenkamp H, Belinfante A (2005) Timed testing with TorX. In: Formal methods Europe (FME), volume 3582 of LNCS, pp 173–188. Springer
Bernardo M, Botta S (2008) A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems. Math Struct Comput Sci 18(01): 29–55
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–173. Springer
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–375
Belinfante AEF (2010) JTorX: a tool for on-line model-driven test derivation and execution, volume 6015 of LNCS, pp 266–270. Springer
Baier C, Katoen J-P, Larsen KG (2008) Principles of model checking. MIT Press, Cambridge
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–82
Böhr F (2011) Model based statistical testing of embedded systems. In: IEEE 4th international conference on software testing, verification and validation workshops (ICSTW), pp 18–25
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–302. Springer
Cleaveland R, Dayar Z, Smolka SA, Yuen S (1999) Testing preorders for probabilistic processes. Inf Comput 154(2): 93–148
Cohn DL (1980) Measure Theory. Birkhäuser, Boston
Cheung L, Stoelinga MIA, Vaandrager FW (2007) A testing scenario for probabilistic processes. J ACM 54(6): 29
Deng Y, Hennessy M, van Glabbeek RJ, Morgan C (2008) Characterising testing preorders for finite probabilistic processes. CoRR
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–273
Goga N (2000) An optimization of the torx test generation algorithm. Xootic Mag 8(2): 15–21
Gerhold M, Stoelinga M (2015) Ioco theory for probabilistic automata. In: Proceedings of tenth workshop on MBT, pp 23–40
Gerhold M, Stoelinga M (2016) Model-based testing of probabilistic systems, pp 251–268. Springer, Berlin
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)
van Glabbeek RJ, Smolka SA, Steffen B, Tofts CMN (1990) Reactive, generative, and stratified models of probabilistic processes, pp 130–141. IEEE Computer Society Press, Philadelphia
MATLAB Users Guide (1998) The Mathworks Inc., Natick, MA, vol 5, pp 333
Hwang I, Cavalli AR (2010) Testing a probabilistic FSM using interval estimation. Comput Netw 54: 1108–1125
Hermanns H (2002) Interactive Markov chains: and the quest for quantified quality. Springer, Berlin
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–117. Springer
Hierons RM, Merayo MG (2009) Mutation testing from probabilistic and stochastic finite state machines. J Syst Softw 82: 1804–1818
Hierons RM, Núñez M (2010) Testing probabilistic distributed systems, volume 6117 of LNCS, pp 63–77. Springer
Hierons RM, Núñez M (2012) Using schedulers to test probabilistic distributed systems. Formal Asp Comput 24(4–6): 679–699
Hierons RM, Núñez M (2017) Implementation relations and probabilistic schedulers in the distributed test architecture. J Syst Softw 132: 319–335
Jeannet B, D’Argenio PR, Larsen KG (2002) Rapture: a tool for verifying Markov decision processes. In: Tools day
Jegourel C, Legay A, Sedwards S (2012) A platform for high performance statistical model checking—PLASMA. Springer, Heidelberg
Jorgensen M, Shepperd M (2007) A systematic review of software development cost estimation studies. IEEE Trans softw Eng 33(1): 33–53
Kwiatkowska M, Norman G, Parker D (2002) PRISM: probabilistic symbolic model checker. In: computer performance evaluation: modelling techniques and tools, pp 200–204. Springer
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–428
Larsen KG, Skou A (1989) Bisimulation through probabilistic testing, pp 344–352. ACM Press, New York
Marsan MA, Balbo G, Conte G, Donatelli S, Franceschinis G (1994) Modelling with generalized stochastic petri nets. Wiley, Hoboken
Milner R (1980) A calculus of communicating systems. Springer, New York
Nie J, Demmel J, Gu M (2008) Global minimization of rational functions and the nearest GCDs. J Glob Optim 40(4): 697–718
De Nicola R, Hennessy MCB (1984) Testing equivalences for processes. Theor Comput Sci 34(1): 83–133
Pfeffer A (2011) Practical probabilistic programming. In: Inductive logic programming, volume 6489 of LNCS, pp 2–3. Springer, Berlin
Peters H, Knieke C, Brox O, Jauns-Seyfried S, Krämer 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–301. Springer
Prowell SJ (2003) Computations for Markov chain usage models. Technical Report
Puterman ML (2014) Markov decision processes: discrete stochastic dynamic programming. Wiley, New York
Paige B, Wood F (2014) A compilation target for probabilistic programming languages. CoRR, arXiv:1403.0504
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’85, volume 10, pp 5–8
Remke A, Stoelinga M (eds) (2014) Stochastic model checking. Rigorous dependability analysis using model checking techniques for stochastic systems—International Autumn School, ROCKS 2012, volume 8453 of LNCS. Springer
Segala R (1995) Modeling, verification of randomized distributed real-time systems. Ph.D. thesis, Cambridge, MA, USA
Segala R (1996) Testing probabilistic automata. In: CONCUR 96: concurrency theory, volume 1119, pp 299–314. Springer
Stoelinga MIA (2002) Alea jacta est: verification of probabilistic, real-time and parametric systems. Ph.D. thesis, Radboud University of Nijmegen
Stokkink WGJ, Timmer M, Stoelinga MIA (2013) Divergent quiescent transistion sytems. In: Proceedings 7th conference on tests and proofs (TAP’13), LNCS
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–74. Springer, Berlin
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–215
Sen K, Viswanathan M, Agha G (2005) On statistical model checking of stochastic systems. In: CAV, pp 266–280
Thrun S, Burgard W, Fox D (2005) Probabilistic robotics. MIT Press, Cambridge
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–32. IOS Press
Tretmans J (1996) Test generation with inputs, outputs and repetitive quiescence. Softw Concepts Tools 17(3): 103–120
Tretmans J (2008) Model based testing with labelled transition systems. In: Formal methods and testing, volume 4949 of LNCS, pp 1–38. Springer
van Osch M (2006) Hybrid input-output conformance and test generation. In: Proceeings of FATES/RV 2006, number 4262 in LNCS, pp 70–84
Walton GH, Poore JH, Trammell CJ (1995) Statistical testing of software based on a usage model. Softw Pract Exp 25(1): 97–108
Whittaker JA, Rekab K, Thomason MG (2000) A Markov chain model for predicting the reliability of multi-build software. Inf Softw Technol 42(12): 889–894
Author information
Authors and Affiliations
Corresponding authors
Additional information
Perdita Stevens, Andrzej Wasowski, and Ewen Denney
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Gerhold, M., Stoelinga, M. Model-based testing of probabilistic systems. Form Asp Comp 30, 77–106 (2018). https://doi.org/10.1007/s00165-017-0440-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0440-4