zbMATH — the first resource for mathematics

Testing from algebraic specifications: Test data set selection by unfolding axioms. (English) Zbl 1183.68175
Grieskamp, Wolfgang (ed.) et al., Formal approaches to software testing. 5th international workshop, FATES 2005, Edinburgh, UK, July 11, 2005. Revised selected papers. Berlin: Springer (ISBN 3-540-34454-3/pbk). Lecture Notes in Computer Science 3997, 203-217 (2006).
Summary: This paper deals with test data set selection from algebraic specifications. Test data sets are generated from selection criteria which are usually defined to cover specification axioms. The unfolding selection criterion consists in covering the input domain of an operation using case analysis. The unfolding procedure can be iterated in order to split input domains of operations into finer subdomains. In this paper we propose to extend an unfolding procedure previously developed in [G. Bernot, M.-C. Gaudel and B. Marre, “Software testing based on formal specifications: a theory and a tool”, Software Engineering Journal 6, No. 6, 387–405 (1991); B. Marre, “Toward an automatic test data set selection using algebraic specifications and logic programming”, in: K. Furukawa (ed.), 8th International Conference on Logic Programming (ICLP ’91), MIT Press, 25–28 (1991)] that could only be performed on very low level, i.e. executable specifications. On the contrary, our new unfolding procedure can be applied to any positive conditional specification. We show that our unfolding procedure is sound (no test is added) and complete (no test is lost) with respect to the starting reference test data set.
For the entire collection see [Zbl 1102.68005].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q65 Abstract data types; algebraic specification
Full Text: DOI
[1] Aiguier, M., Arnould, A., Boin, C., Le Gall, P., Marre, B.: Testing from algebraic specifications: Test data set selection by unfolding axioms. Rapport LaMI 110, Université d’Évry-Val d’Essonne (2005), ftp://ftp.lami.univ-evry.fr/pub/publications/reports · Zbl 1183.68175
[2] Arnould, A., Le Gall, P.: Test de conformité: une approche algébrique. Technique et Science Informatiques, Test de logiciel 21(9), 1219–1242 (2002)
[3] Arnould, A., Le Gall, P., Marre, B.: Dynamic testing from bounded data type specifications. In: Hlawiczka, A., Simoncini, L., Silva, J.G.S. (eds.) EDCC 1996. LNCS, vol. 1150, pp. 285–302. Springer, Heidelberg (1996)
[4] Bernot, G.: Testing against formal specifications: a theoretical view. In: Abramsky, S. (ed.) TAPSOFT 1991, CCPSD 1991, and ADC-Talks 1991. LNCS, vol. 494, pp. 99–119. Springer, Heidelberg (1991) · doi:10.1007/3540539816_63
[5] Bernot, G., Gaudel, M.-C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Software Engineering Journal 6(6), 387–405 (1991) · doi:10.1049/sej.1991.0040
[6] Bernot, G., Bouaziz, L., Le Gall, P.: A theory of probabilistic functional testing. In: ICSE 1997: Proceedings of the 19th international conference on Software engineering, pp. 216–226. ACM Press, New York (1997)
[7] Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Science of Computer Programming 25(2-3), 149–186 (1995) · Zbl 0853.68130 · doi:10.1016/0167-6423(95)00014-3
[8] Brucker, A.D., Wolff, B.: Symbolic test case generation for primitive recursive functions. In: Formal Approaches to Testing of Software (to appear, 2004) · Zbl 1081.68672
[9] Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of haskell programs. In: International Conference on Functional Programming, pp. 268–279 (2000) · Zbl 06481641 · doi:10.1145/351240.351266
[10] Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 268–284. Springer, Heidelberg (1993) · doi:10.1007/BFb0024651
[11] Doche, M., Wiels, V.: Extended institutions for testing. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 514–528. Springer, Heidelberg (2000) · Zbl 0983.68038 · doi:10.1007/3-540-45499-3_36
[12] Gaudel, M.C.: Testing can be formal, too. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 82–96. Springer, Heidelberg (1995) · doi:10.1007/3-540-59293-8_188
[13] Jouannaud, J.-P., Waldmann, B.: Reductive conditional term rewriting systems. In: Wirsing, M. (ed.) 3rd IFIP Conference on Formal Description of Programming Concepts, Elsevier Science Publishers, Amsterdam (1985)
[14] Le Gall, P., Arnould, A.: Formal specification and test: correctness and oracle. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 342–358. Springer, Heidelberg (1996) · doi:10.1007/3-540-61629-2_52
[15] Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - A survey. In: Proceedings of the IEEE, vol. 84, pp. 1090–1126 (1996) · doi:10.1109/5.533956
[16] Legeard, B., Peureux, F., Utting, M.: Controlling test case explosion in test generation from b formal models. Softw. Test., Verif. Reliab. 14(2), 81–103 (2004) · Zbl 05446736 · doi:10.1002/stvr.287
[17] Machado, P.: Testing from structured algebraic specifications. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 529–544. Springer, Heidelberg (2000) · Zbl 0983.68122 · doi:10.1007/3-540-45499-3_37
[18] Machado, P., Sannella, D.: Unit testing for casl architectural specifications. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 506–518. Springer, Heidelberg (2002) · Zbl 1014.68100 · doi:10.1007/3-540-45687-2_42
[19] Marre, B.: Toward an automatic test data set selection using algebraic specifications and logic programming. In: Furukawa, K. (ed.) Eight International Conference on Logic Programming (ICLP 1991), pp. 25–28. MIT Press, Cambridge (1991)
[20] Marre, B., Arnould, A.: Test sequences generation from LUSTRE descriptions: GATEL. In: ASE-00: The 15th IEEE Conference on Automated Software Engineering, Grenoble, September 2000, pp. 229–237. IEEE CS Press, Los Alamitos (2000) · doi:10.1109/ASE.2000.873667
[21] Marre, B., Blanc, B.: Test selection strategies for lustre descriptions in gatel. In: MBT 2004 joint to ETAPS 2004. ENTCS, vol. 111, pp. 93–111 (2004)
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.