zbMATH — the first resource for mathematics

Test selection criteria for quantifier-free first-order specifications. (English) Zbl 1141.68447
Arbab, Farhad (ed.) et al., International symposium on fundamentals of software engineering. International symposium, FSEN 2007, Tehran, Iran, April 17–19, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75697-2/pbk). Lecture Notes in Computer Science 4767, 144-159 (2007).
Summary: 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.
For the entire collection see [Zbl 1138.68001].

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
Full Text: DOI