Abstract
Testing from first-order specifications has mainly been studied for flat specifications, that are specifications of a single software module. However, the specifications of large software systems are generally built out of small specifications of individual modules, by enriching their union. The aim of integration testing is to test the composition of modules assuming that they have previously been verified, i.e. assuming their correctness. One of the main method for the selection of test cases from first-order specifications, called axiom unfolding, is based on a proof search for the different instances of the property to be tested, thus allowing the coverage of this property. The idea here is to use deduction modulo as a proof system for structured first-order specifications in the context of integration testing, so as to take advantage of the knowledge of the correctness of the individual modules.
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
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)
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)
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)
Wirsing, M.: Algebraic specification. In: Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, ch. 13, pp. 675–788. Elsevier, Amsterdam (1990)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)
Machado, P.: Testing from structured algebraic specifications. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 529–544. Springer, Heidelberg (2000)
Doche, M., Wiels, V.: Extended institutions for testing. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 514–528. Springer, Heidelberg (2000)
Aiguier, M., Arnould, A., Le Gall, P., Longuet, D.: Exhaustive test sets for algebraic specification correctness. Technical report, IBISC, Université d’Évry (2008)
Ohlebush, E.: Modular properties of composable term rewriting systems. Journal of Symbolic Computation 20, 1–41 (1995)
Aiguier, M., Arnould, A., Le Gall, P., Longuet, D.: Test selection criteria from quantifier-free first-order specifications. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 144–159. Springer, Heidelberg (2007)
Longuet, D., Aiguier, M., Le Gall, P.: Proof-guided test selection from first-order specifications with equality. Journal of Automated Reasoning (to appear, 2009)
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)
Orejas, F., Navarro, M., Sánchez, A.: Implementation and behavioural equivalence: a survey. In: Bidoit, M., Choppy, C. (eds.) Abstract Data Types 1991 and COMPASS 1991. LNCS, vol. 655, pp. 144–163. Springer, Heidelberg (1993)
Longuet, D., Aiguier, M.: Integration testing from structured first-order specifications via deduction modulo. Technical report, LSV, ENS Cachan (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Longuet, D., Aiguier, M. (2009). Integration Testing from Structured First-Order Specifications via Deduction Modulo. In: Leucker, M., Morgan, C. (eds) Theoretical Aspects of Computing - ICTAC 2009. ICTAC 2009. Lecture Notes in Computer Science, vol 5684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03466-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-03466-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03465-7
Online ISBN: 978-3-642-03466-4
eBook Packages: Computer ScienceComputer Science (R0)