Abstract
This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulae. Test cases are modeled as ground formulae and any specification has an exhaustive test data set whose successful submission means correctness, provided that the software under verification can be modeled as a first-order structure over the same signature. As it has already been done for positive conditional equational specifications, we derive test cases from selection criteria based on axiom coverage. Our selection criteria allows us to select test cases by iteratively unfolding an initial target test purpose, given as a formula. The initial reference test set is iteratively split into successive subsets. Each subset of test cases is defined by constraints which are increasingly introduced by the unfolding procedure to ensure an appropriate matching between the current test purpose under unfolding and specification axioms. Our unfolding procedure is sound (no test is added) and complete (no test is lost) with respect to the starting test purpose. It is exemplified on a simple example.
This work is performed within a French national project STACS (Spécification et Test, Abstraits et Compositionnels, de Systèmes) in collaboration with the French Atomic Energy Commission (CEA). This project is devoted to automatically generate test data sets for Input Output Symbolic Transition Systems.
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
Le Gall, P., Arnould, A.: Formal specification and test: correctness and oracle. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Recent Trends in Data Type Specification. LNCS, vol. 1130, pp. 342–358. Springer, Heidelberg (1996)
Gaudel, M.: 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)
Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software—Concepts and Tools 17(3), 103–120 (1996)
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)
Marre, B.: Loft: a tool for assisting selection of test data sets from algebraic specifications. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 799–800. Springer, Heidelberg (1995)
Aiguier, M., Arnould, A., Boin, C., Le Gall, P., Marre, B.: Testing from algebraic specifications: Test data set selection by unfolding axioms. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol. 3997, pp. 203–217. Springer, Heidelberg (2006)
Machado, P.: On oracles for interpreting test results against algebraic specifications. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, Springer, Heidelberg (1998)
Machado, P.: Testing from structured algebraic specifications. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 529–544. Springer, Heidelberg (2000)
Arnould, A., Le Gall, P.: Test de conformité: une approche algébrique. Technique et Science Informatiques, Test de logiciel 21, 1219–1242 (2002)
Arnould, A., Le Gall, P., Marre, B.: Dynamic testing from bounded data type specifications. In: Hlawiczka, A., Simoncini, L., Silva, J.G.S. (eds.) Dependable Computing - EDCC-2. LNCS, vol. 1150, pp. 285–302. Springer, Heidelberg (1996)
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)
Aiguier, M., Arnould, A., Le Gall, P.: Exhaustive test sets for algebraic specification correctness. Technical report, IBISC - Université d’Évry Val d’Essonne (2006)
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)
Hennicker, R., Wirsing, M., Bidoit, M.: Proof systems for structured specifications with observability operators. Theoretical Computer Science 173(2), 393–443 (1997)
Aiguier, M., Arnould, A., Le Gall, P., Longuet, D.: Test selection criteria for quantifier-free first-order specifications. Technical Report, -01, IBISC - Université d’Évry Val d’Essonne (2007), available at http://www.ibisc.fr/~dlonguet/Publications/RR-AALL07.pdf
Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York (1986)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aiguier, M., Arnould, A., Le Gall, P., Longuet, D. (2007). Test Selection Criteria for Quantifier-Free First-Order Specifications. In: Arbab, F., Sirjani, M. (eds) International Symposium on Fundamentals of Software Engineering. FSEN 2007. Lecture Notes in Computer Science, vol 4767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75698-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-75698-9_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75697-2
Online ISBN: 978-3-540-75698-9
eBook Packages: Computer ScienceComputer Science (R0)