Abstract
Model-based Debugging is an application of Model-based Diagnosis techniques to debugging computer systems. Its basic principle is to compare a model, i.e., a description of the correct behaviour of a system, to the observed behaviour of the system. In this paper we show how this technique can be applied in the context of model-based mutation testing (MBMT) with timed automata. In MBMT we automatically generate a set of test sequences out of a test model. In contrast to general model-based testing, the test cases of MBMT cover a pre-defined set of faults that have been injected into the model (model mutation). Our automatic debugging process is purely black-box. If a test run fails, our tool reports a diagnosis as a set of model mutations. These mutations provide possible explanations why the test case has failed. For reproducing the failure, we also generate a set of minimal test cases leading to the implementation fault. The technique is implemented for Uppaal’s timed automata models and is based on a language inclusion check via bounded model checking. It adds debugging capability to our existing test-case generators. A car-alarm system serves as illustrating case study.
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
Aichernig, B.K., Brandl, H., Jöbstl, E., Krenn, W.: Efficient mutation killers in action. In: ICST, pp. 120–129 (2011)
Aichernig, B.K., Brandl, H., Jöbstl, E., Krenn, W.: UML in action: A two-layered interpretation for testing. ACM SIGSOFT SEN 36(1), 1–8 (2011)
Aichernig, B.K., Lorber, F., Ničković, D.: Time for mutants - model-based mutation testing with timed automata. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 20–38. Springer, Heidelberg (2013)
Aichernig, B.K., Lorber, F., Ničković, D.: Model-based mutation testing with timed automata. Technical Report IST-MBT-2013-02, TU Graz (2013), http://www.ist.tugraz.at/aichernig/publications/papers/IST-MBT-2013-02.pdf
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Brillout, A., He, N., Mazzucchi, M., Kroening, D., Purandare, M., Rümmer, P., Weissenbacher, G.: Mutation-based test case generation for Simulink models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 208–227. Springer, Heidelberg (2010)
DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Hints on test data selection: Help for the practicing programmer. Computer 11(4), 34–41 (1978)
He, N., Rümmer, P., Kroening, D.: Test-case generation for embedded Simulink via formal concept analysis. In: DAC, pp. 224–229 (2011)
Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Transactions on Software Engineering 37(5), 649–678 (2011)
Krenn, W., Ničković, D., Tec, L.: Incremental language inclusion checking for networks of timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 152–167. Springer, Heidelberg (2013)
Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Formal Methods in System Design 34(3), 238–304 (2009)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1-2), 134–152 (1997)
Mayer, W., Stumptner, M.: Model-based debugging - state of the art and future challenges. Electr. Notes Theor. Comput. Sci. 174(4), 61–82 (2007)
Mayer, W., Stumptner, M.: Evaluating models for model-based debugging. In: ASE, pp. 128–137. IEEE (2008)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Nica, M., Nica, S., Wotawa, F.: Does testing help to reduce the number of potentially faulty statements in debugging? In: Bottaci, L., Fraser, G. (eds.) TAIC PART 2010. LNCS, vol. 6303, pp. 88–103. Springer, Heidelberg (2010)
Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)
Schlick, R., Herzner, W., Jöbstl, E.: Fault-based generation of test cases from UML-models: Approach and some experiences. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 270–283. Springer, Heidelberg (2011)
Schmaltz, J., Tretmans, J.: On conformance testing for timed systems. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 250–264. Springer, Heidelberg (2008)
Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)
Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software - Concepts and Tools 17(3), 103–120 (1996)
Wotawa, F.: On the relationship between model-based debugging and program mutation. Artificial Intelligence 135, 2002 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Aichernig, B.K., Hörmaier, K., Lorber, F. (2014). Debugging with Timed Automata Mutations. In: Bondavalli, A., Di Giandomenico, F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science, vol 8666. Springer, Cham. https://doi.org/10.1007/978-3-319-10506-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-10506-2_4
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10505-5
Online ISBN: 978-3-319-10506-2
eBook Packages: Computer ScienceComputer Science (R0)