# zbMATH — the first resource for mathematics

Proof-guided test selection from first-order specifications with equality. (English) Zbl 1214.68221
Summary: This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ideal exhaustive test set to start the selection from. We then propose an extension of the test selection method called axiom unfolding, originally defined for algebraic specifications, to quantifier-free first-order specifications with equality. This method basically consists of a case analysis of the property under test (the test purpose) according to the specification axioms. It is based on a proof search for the different instances of the test purpose. Since the calculus is sound and complete, this allows us to provide a full coverage of this property. The generalisation we propose allows to deal with any kind of predicate (not only equality) and with any form of axiom and test purpose (not only equations or Horn clauses). Moreover, it improves our previous works with efficiently dealing with the equality predicate, thanks to the paramodulation rule.

##### MSC:
 68Q60 Specification and verification (program logics, model checking, etc.)
CASL; QuickCheck
Full Text:
##### References:
 [1] Aiguier, M., Arnould, A., Boin, C., Le Gall, P., Marre, B.: Testing from algebraic specifications: test data set selection by unfolding axioms. In: Formal Approaches to Testing of Software (FATES’05). Lecture Notes in Computer Science, vol. 3997, pp. 203–217. Springer, New York (2005) · Zbl 1183.68175 [2] Aiguier, M., Arnould, A., Le Gall, P., Longuet, D.: Test selection criteria from quantifier-free first-order specifications. In: Fundamentals of Software Engineering (FSEN’07). Lecture Notes in Computer Science, vol. 4767, pp. 144–159. Springer, New York (2007) · Zbl 1141.68447 [3] Aiguier, M., Arnould, A., Le Gall, P., Longuet, D.: Exhaustive test sets for algebraic specification correctness. Technical report, IBISC, Université d’Évry Val d’Essonne (2008). http://www.epigenomique.genopole.fr/iguier/publications/communications/exhaust.pdf · Zbl 1141.68447 [4] Arnould, A., Le Gall, P.: Test de conformité : une approche algébrique. TSI. Tech. Sci. Inform. Test de logiciel 21, 1219–1242 (2002) [5] Arnould, A., Le Gall, P., Marre, B.: Dynamic testing from bounded data type specifications. In: Dependable Computing–EDCC-2. Lecture Notes in Computer Science, vol. 1150, pp. 285–302. Springer, New York (1996) [6] Bernot, G.: Testing against formal specifications: a theoretical view. In: Theory and Practice of Software Development (TAPSOFT’91). Lecture Notes in Computer Science, vol. 494, pp. 99–119. Springer, New York (1991) [7] Bernot, G., Gaudel, M.-C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Softw. Eng. J. 6(6), 387–405 (1991) · doi:10.1049/sej.1991.0040 [8] Brucker, A.D., Wolff, B.: Symbolic test case generation for primitive recursive functions. In: Formal Approaches to Software Testing (FATES’04). Lecture Notes in Computer Science, vol. 3395, pp. 16–32. Springer, New York (2004) [9] Carlier, M., Duboism, C.: Functional testing in the focal environment. In: Tests and Proofs (TAP’08). Lecture Notes in Computer Science, vol. 4966, pp. 84–98. Springer, New York (2008) [10] Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Not. 35(9), 268–279 (2000) · doi:10.1145/357766.351266 [11] Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Formal Methods Europe (FME’93). Lecture Notes in Computer Science, vol. 670, pp. 268–284. Springer, New York (1993) [12] Frantzen, L., Tretmans, J., Willemse, T.A.C.: Test generation based on symbolic specifications. In: Formal Approaches to Software Testing (FATES’04). Lecture Notes in Computer Science, vol. 3395, pp. 1–15. Springer, New York (2004) · Zbl 1081.68570 [13] Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for test purpose definition. In: Testing of Communicating Systems (TestCom’06). Lecture Notes in Computer Science, vol. 3964, pp. 1–18. Springer, New York (2006) · Zbl 1185.68413 [14] Gaudel, M.-C.: Testing can be formal, too. In: Theory and Practice of Software Development (TASPOFT’95). Lecture Notes in Computer Science, vol. 915, pp. 82–96. Springer, New York (1995) [15] Gaudel, M.-C., Le Gall, P.: Testing data types implementations from algebraic specifications. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. Lecture Notes in Computer Science, vol. 4949, pp. 209–239. Springer, New York (2008) [16] Hennicker, R., Wirsing, M., Bidoit, M.: Proof systems for structured specifications with observability operators. Theor. Comp. Sci. 173(2), 393–443 (1997) · Zbl 0901.68116 · doi:10.1016/S0304-3975(96)00162-4 [17] Jard, C., Jéron, T.: TGV: theory, principles and algorithms. A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Int. J. Softw. Tools Technol. Transf. 6, 297–315 (2004) [18] Koopman, P.W.M., Alimarine, A., Tretmans, J., Plasmeijer, M.J.: GAST: generic automated software testing. In: Implementation of Functional Languages. Lecture Notes in Computer Science, vol. 2670, pp. 84–100. Springer, New York (2002) [19] Le Gall, P., Arnould, A.: Formal specification and test: correctness and oracle. In: 11th Workshop on Algebraic Development Techniques (WADT’96). Lecture Notes in Computer Science, vol. 1130, pp. 342–358. Springer, New York (1996) [20] Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines–a survey. Proc. IEEE 84, 1090–1126 (1996) · doi:10.1109/5.533956 [21] Lussier, G., Waeselynck, H.: Proof-guided test: an experimental study. In: International Computer Software and Applications Conference (COMPSAC’04), pp. 528–533. IEEE Computer Society, Los Alamitos (2004) [22] Machado, P.: On oracles for interpreting test results against algebraic specifications. In: Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, vol. 1548. Springer, New York (1999) [23] Machado, P.: Testing from structured algebraic specifications. In: Algebraic Methodology and Software Technology (AMAST’00). Lecture Notes in Computer Science, vol. 1816, pp. 529–544. Springer, New York (2000) · Zbl 0983.68122 [24] Machado, P., Sannella, D.: Unit testing for Casl architectural specifications. In: Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 2420, pp. 506–518. Springer, New York (2002) · Zbl 1014.68100 [25] Marre, B.: LOFT : a tool for assisting selection of test data sets from algebraic specifications. In: Theory and Practice of Software Development (TAPSOFT’95). Lecture Notes in Computer Science, vol. 915, pp. 799–800. Springer, New York (1995) [26] Mosses, P.D.: CASL reference manual, the complete documentation of the common algebraic specification language. Lecture Notes in Computer Science, vol. 2960. Springer, New York (2004) · Zbl 1046.68001 [27] Petrenko, A., Boroday, S., Groz, R.: Confirming configurations in EFSM. In: Formal Methods for Protocol Engineering and Distributed Systems (FORTE’99). IFIP Conference Proceedings, vol. 156, pp. 5–24. Springer, New York (1999) · Zbl 0952.68092 [28] Phalippou, M.: Relations d’implantation et hypothèses de test sur les automates à entrées et sorties. PhD thesis, Université de Bordeaux (1994) [29] Robinson, G.A., Wos, L.: Paramodulation and theorem proving in first-order theories with equality. Mach. Intell. 4, 133–150 (1969) · Zbl 0219.68047 [30] Rusu, V., du Bousquet, L., Jéron, T.: An approach to symbolic test generation. In: 2nd International Workshop on Integrated Formal Method (IFM’00). Lecture Notes in Computer Science, vol. 1945, pp. 338–357. Springer, New York (2000) · Zbl 1043.68543 [31] Tretmans, J.: Testing labelled transition systems with inputs and outputs. In: International Workshop on Protocols Test Systems (IWPTS’95), Evry, 4–6 September 1995
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.