Abstract
We combine model-based testing and mutation testing to automatically generate a test suite that achieves a high mutation adequacy score. The original model representing the system under test is mutated. To generate test cases that detect whether a modelled fault has been implemented, we perform a refinement check between the original and the mutated models. Action systems serve as formal models. They are well-suited to model reactive systems and allow non-determinism. We extend our previous work by two techniques to improve efficiency: (1) a strategy to efficiently handle a large number of mutants and (2) incremental solving. A case study illustrates the potential of our improvements. The runtime for checking appr. 200 mutants could be reduced from 20s to 3s. We implemented our algorithms in two versions: one uses a constraint solver, the other one an SMT solver. Both show similar performance.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Aichernig, B.K., Brandl, H., Jöbstl, E., Krenn, W.: Efficient mutation killers in action. In: ICST, pp. 120–129. IEEE (2011)
Aichernig, B.K., He, J.: Mutation testing in UTP. Formal Aspects of Computing 21(1-2), 33–64 (2009)
Aichernig, B.K., Jöbstl, E.: Efficient refinement checking for model-based mutation testing. In: QSIC, pp. 21–30. IEEE (2012)
Aichernig, B.K., Jöbstl, E.: Towards symbolic model-based mutation testing: Combining reachability and refinement checking. In: MBT. EPTCS, vol. 80, pp. 88–102 (2012)
Aichernig, B.K., Jöbstl, E.: Towards symbolic model-based mutation testing: Pitfalls in expressing semantics as constraints. In: ICST, pp. 752–757. IEEE (2012)
Aichernig, B.K., Peischl, B., Weiglhofer, M., Wotawa, F.: Protocol conformance testing a SIP registrar: An industrial application of formal methods. In: SEFM, pp. 215–224. IEEE (2007)
Ammann, P., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: ICFEM, pp. 46–54. IEEE (1998)
Back, R.J., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: PODC, pp. 131–142. ACM (1983)
Back, R.J., Sere, K.: Stepwise refinement of action systems. Structured Programming 12, 17–30 (1991)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. STTT 9, 505–525 (2007)
Boroday, S., Petrenko, A., Groz, R.: Can a model checker generate tests for non-deterministic systems? Electr. Notes Theor. Comput. Sci. 190(2), 3–19 (2007)
Budd, T.A., Gopal, A.S.: Program testing by specification mutation. Computer Languages 10(1), 63–73 (1985)
Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191–206. Springer, Heidelberg (1997)
DeMillo, R., Lipton, R., Sayward, F.: Hints on test data selection: Help for the practicing programmer. IEEE Computer 11(4), 34–41 (1978)
Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer (1990)
Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215–261 (2009)
Gotlieb, A., Botella, B., Rueher, M.: Automatic test data generation using constraint solving techniques. In: ISSTA, pp. 53–62 (1998)
Hamlet, R.G.: Testing programs with the aid of a compiler. IEEE Trans. Software Eng. 3(4), 279–290 (1977)
Hoare, C., He, J.: Unifying Theories of Programming. Prentice-Hall (1998)
Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Software Eng. 37(5), 649–678 (2011)
Nogueira, S., Sampaio, A., Mota, A.M.: Guided test generation from CSP models. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 258–273. Springer, Heidelberg (2008)
Okun, V., Black, P.E., Yesha, Y.: Testing with model checker: Insuring fault visibility. In: 2002 WSEAS Int. Conf. on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems, pp. 1351–1356 (2003)
Roscoe, A.W.: Model-checking CSP, ch. 21. Prentice-Hall (1994)
Stocks, P.A.: Applying formal methods to software testing. Ph.D. thesis, Department of computer science, University of Queensland (1993)
Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software - Concepts and Tools 17(3), 103–120 (1996)
Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. (2011)
Whittemore, J., Kim, J., Sakallah, K.: SATIRE: A new incremental satisfiability engine. In: DAC, pp. 542–545. ACM (2001)
Wotawa, F., Nica, M., Aichernig, B.K.: Generating distinguishing tests using the Minion constraint solver. In: ICST, pp. 325–330. IEEE (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aichernig, B.K., Jöbstl, E., Kegele, M. (2013). Incremental Refinement Checking for Test Case Generation. In: Veanes, M., Viganò, L. (eds) Tests and Proofs. TAP 2013. Lecture Notes in Computer Science, vol 7942. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38916-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-38916-0_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38915-3
Online ISBN: 978-3-642-38916-0
eBook Packages: Computer ScienceComputer Science (R0)