Abstract
Randomized testing is a lightweight approach for searching for bugs. It presents a tradeoff between the number of testing experiments performed and the probability to find errors. An important challenge in random testing is when the errors that we try to detect are scattered with very low probability among the different executions, forming a “rare event”. We suggest here the use of a “biasing automaton”, which observes the tested sequence and controls the distribution of the different choices of extending it. By the careful selection of a biasing automaton, we can increase the chance of errors to be found and consequently reduce the number of tests we need to perform. The biasing automaton is constructed through repeated testing of variants of the system under test. We show how to construct biasing automata based on genetic programming.
The research in this paper was partially funded by an ISF-NSFC grant “Runtime Measuring and Checking of Cyber Physical Systems” (ISF award 2239/15, NSFC No. 61561146394). The authors from Nanjing University were also partially funded by a National Natural Science Foundation of China grant No. 61572249.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
For the case of two processes, \(D(s_i, p2) = 1- D(s_i, p1)\), hence this is a unique function of the distributions. In case of k choices, we need to use \(k-1\) parameters for each state.
References
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)
Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008)
Bu, L., Peled, D., Shen, D., Zhuang, Y.: Genetic synthesis of concurrent code using mode checking and statistical model checking. In: SPIN 2018, pp. 275–291 (2018)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Holland, J.H.: Adaptation in Natural and Artificial Systems: An Introductory Analysis with Applications to Biology, Control and Artificial Intelligence. MIT Press, Cambridge (1992)
Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, New Jersey (2004)
Grosu, R., Smolka, S.A.: Monte Carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271–286. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_18
Jegourel, C., Legay, A., Sedwards, S.: An effective heuristic for adaptive importance splitting in statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 143–159. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45231-8_11
Johnson, C.G.: Genetic programming with fitness based on model checking. In: Ebner, M., O’Neill, M., Ekárt, A., Vanneschi, L., Esparcia-Alcázar, A.I. (eds.) EuroGP 2007. LNCS, vol. 4445, pp. 114–124. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71605-1_11
Katz, G., Peled, D.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 141–156. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_11
Gal Katz, D.: Peled: Synthesizing, correcting and improving code, using model checking-based genetic programming. STTT 19(4), 449–464 (2017)
Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge (1992)
Larsen, K.G., Legay, A.: On the power of statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 843–862. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_62
Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_11
Pretschner, A., Holling, D., Eschbach, R., Gemmar, M.: A generic fault model for quality assurance. In: Moreira, A., Schätz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol. 8107, pp. 87–103. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41533-3_6
Kirkpatrick, S., Gelatt Jr., C.D., Vecchi, M.P.: Optimization by simulated annealing. Science 220(4598), 671–680 (1983)
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_17
Acknowledgements
The second author would like to thank Sergiy Bogomolov and Ken McMillan for interesting discussions on this subject.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Bu, L., Peled, D., Shen, D., Tzirulnikov, Y. (2018). Chasing Errors Using Biasing Automata. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. ISoLA 2018. Lecture Notes in Computer Science(), vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-03421-4_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03420-7
Online ISBN: 978-3-030-03421-4
eBook Packages: Computer ScienceComputer Science (R0)