zbMATH — the first resource for mathematics

Test generation from event system abstractions to cover their states and transitions. (English. Russian original) Zbl 1455.68104
Program. Comput. Softw. 44, No. 1, 1-14 (2018); translation from Programmirovanie 44, No. 1, 3-20 (2018).
Summary: Model-based testing of event systems can take advantage of considering abstractions rather than explicit models, for controlling their size. When abstracting still a test has to be a concrete connected and reachable event sequence. This paper presents a test generation method based on computing a reachable and connected under-approximation of the abstraction of an event system. We compute the under-approximation with concrete instances of the abstract transitions, that cover all the states and transitions of the predicatebased abstraction. We propose an algorithmic method that instantiates each of the abstract transitions, and maintains for widening it a frontier of concretely reached states. We present heuristics to favour the instances connectivity. The idea is to prolong whenever possible the already reached sequences of concrete transitions, and to parameterize the order in which the states and actions occur. This concrete under-approximation ends up covering partially (at best totally) the reachable abstract transitions. The computed tests are paths of the under-approximation. The paper also reports on an implementation, which permits to provide experimental results confirming the interest of the approach with related heuristics.
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Graf, S.; Saidi, H., Construction of abstract state graphs with PVS, 72-83 (1997)
[2] Godefroid, P.; Jagadeesan, R., On the expressiveness of 3-valued models, 206-222 (2003) · Zbl 1022.68075
[3] Abrial, J.-R., Modeling in Event-B: System and Software Design, Cambridge Univ. Press, 2010. · Zbl 1213.68214
[4] Dijkstra, E.W., Guarded commands, nondeterminacy, and formal derivation of programs, Commun. ACM, 1975, vol. 18, no. 8, pp. 453-457. · Zbl 0308.68017
[5] Dijkstra, E.W., A Discipline of Programming, Prentice-Hall, 1976. · Zbl 0368.68005
[6] Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 2003, vol. 50, no. 5, pp. 752-794. · Zbl 1325.68145
[7] Veanes, M.; Yavorsky, R., Combined algorithm for approximating a finite state abstraction of a large system, 86-91 (2003)
[8] Abrial, J.-R., The B Book, Cambridge Univ. Press, 1996. · Zbl 0915.68015
[9] Gurevich, Y., Sequential abstract-state machines capture sequential algorithms, ACM Trans. Computational Logic, 2000, vol. 1, no. 1, pp. 77-111. · Zbl 1365.68258
[10] Abstract State Machines, Gurevich, Y., Kutter, P.W., Odersky, M., and Thiele, L., Eds., Theory and Applications, vol. 1912 of LNCS, Springer, 2000.
[11] Bert, D.; Cave, F., Construction of finite labeled transition systems from B abstract systems, 235-254 (2000) · Zbl 1043.68586
[12] Bride, H., Julliand, J., and Masson, P.-A., Tri-modal under-approximation for test generation, Sci. Comput. Program., 2016, vol. 132, no. P2, pp. 190-208.
[13] Cousot, P. and Cousot, R., Abstract interpretation frameworks, J. Logic Computation, 1992, vol. 2, no. 4, pp. 511-547. · Zbl 0783.68073
[14] Ball, T., A theory of predicate-complete test coverage and generation, 1-22 (2004) · Zbl 1143.68361
[15] Godefroid, P.; Huth, M.; Jagadeesan, R., Abstraction-based model checking using modal transition systems, 426-440 (2001) · Zbl 1006.68077
[16] Larsen, K. G.; Thomsen, B., A modal process logic, 203-210 (1988)
[17] Grieskamp, W.; Gurevich, Y.; Schulte, W.; Veanes, M., Generating finite state machines from abstract state machines, 112-122 (2002)
[18] Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., and Pretschner, A., Model-Based Testing of Reactive Systems, vol. 3472 of LNCS, Springer, 2005. · Zbl 1070.68088
[19] Utting, M. and Legeard, B., Practical Model-Based Testing, Morgan Kaufmann, 2006.
[20] Thimbleby, H.W., The directed Chinese postman problem, Software: Practice and Experience, 2003, vol. 33, no. 11, pp. 1081-1096.
[21] Dwyer, M. B.; Avrunin, G. S.; Corbett, J. C., Patterns in property specifications for finite-state verification, 411-420 (1999)
[22] Moura, L.; Bjorner, N., An efficient SMT solver, 337-340 (2008)
[23] Bué, P.-C.; Julliand, J.; Masson, P.-A., Association of under-approximation techniques for generating tests from models, 51-68 (2011) · Zbl 1335.68046
[24] Julliand, J.; Kouchnarenko, O.; Masson, P.-A.; Voiron, G., Two under-approximation techniques for 3-modal abstraction coverage of event systems: Joint effort (2017)
[25] Aichernig, B.K., Brandl, H., Jöbstl, E., and Krenn, W., UML in action: A two-layered interpretation for testing, ACM SIGSOFT Software Eng. Notes, 2011, vol. 36, no. 1, pp. 1-8.
[26] Microsoft Corporation, Abstract state machine language. https://asml.codeplex.com/.
[27] FP7 Deploy Project, Industrial deployment of system engineering methods providing high dependability and productivity. http://www.deploy-project.eu/index.html.
[28] Namjoshi, K. S.; Kurshan, R. P., Syntactic program transformations for automatic abstraction, 435-449 (2000) · Zbl 0974.68524
[29] Pasareanu, C.S., Peláanek, R., and Visser, W., Predicate abstraction with under-approximation refinement, Logic Methods Comput. Sci., 2007, vol. 3, no. 1, pp. 1-22. · Zbl 1128.68054
[30] Gulavani, B. S.; Henzinger, T. A.; Kannan, Y.; Nori, A. V.; Rajamani, S. K., SYNERGY: A new algorithm for property checking, 117-127 (2006)
[31] Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J., Tetali, S.D., and Thakur, A.V., Proofs from tests, IEEE Trans. Software Eng., 2010, vol. 36, no. 4, pp. 495-508.
[32] Rapin, N.; Gaston, C.; Lapitre, A.; Gallois, J.-P., Behavioral unfolding of formal specifications based on communicating extended automata (2003)
[33] Godefroid, P.; Klarlund, N.; Sen, K., DART: Directed automated random testing, 213-223 (2005)
[34] Sen, K.; Marinov, D.; Agha, G., CUTE: a concolic unit testing engine for C, 263-272 (2005)
[35] Cadar, C.; Ganesh, V.; Pawlowski, P. M.; Dill, D. L.; Engler, D. R., EXE: Automatically generating inputs of death, 322-335 (2006)
[36] Tillmann, N.; Halleux, J., Pex-white box test generation for NET, 134-153 (2008)
[37] Pasareanu, C.S. and Visser, W., A survey of new trends in symbolic execution for software testing and analysis, STTT, 2009, vol. 11, no. 4, pp. 339-353.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.