Exhaustive test sets for algebraic specification correctness

Autor: Aiguier, Marc, Arnould, Agnès, Le Gall, Pascale, Longuet, Delphine
Přispěvatelé: Mathématiques et Informatique pour la Complexité et les Systèmes (MICS), CentraleSupélec, Synthèse et analyse d'images (XLIM-ASALI), XLIM (XLIM), Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS)-Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS), Université de Poitiers, ForTesse, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
Jazyk: angličtina
Rok vydání: 2016
Předmět:
Zdroj: Journal of : Software Testing, Verification and Reliability
Journal of : Software Testing, Verification and Reliability, Wiley, 2016, 26 (4), pp.294-317. ⟨10.1002/stvr.1598⟩
ISSN: 0960-0833
1099-1689
DOI: 10.1002/stvr.1598⟩
Popis: International audience; In the context of testing from algebraic specifications, test cases are ground formulas chosen amongst the ground semantic consequences of the specification, according to some possible additional observability conditions. A test set is said to be exhaustive if every programme P passing all the tests is correct and if for every incorrect programme P, there exists a test case on which P fails. Because correctness can be proved by testing on such a test set, it is an appropriate basis for the selection of a test set of practical size. The largest candidate test set is the set of observable consequences of the specification. However, depending on the nature of specifications and programmes, this set is not necessarily exhaustive. In this paper, we study conditions to ensure the exhaustiveness property of this set for several algebraic formalisms (equational, conditional positive, quantifier free and with quantifiers) and several test hypotheses.
Databáze: OpenAIRE
Externí odkaz: