| Authors: |
Engin Uzuncaova
and Daniel Garcia
and Sarfraz Khurshid
and Don S. Batory
|
| Editors: |
Ivica Crnkovic
and Antonia Bertolino
|
| URL: |
http://doi.acm.org/10.1145/1287624.1287701 |
| Description: |
Computer Science Bibliography Collection |
| Tags: |
AHEAD
Alloy
GenVoca
generation
line
product
specification-based
testdata
testing
|
| Abstract: |
This paper presents a specification-based approach for sys-
tematic testing of products from a software product line.
Our approach uses specifications given as formulas in Alloy,
a first-order logic based on relations. Alloy formulas can
be checked for satisfiability using the Alloy Analyzer. The
fully automatic analyzer, given an Alloy formula and a scope,
i.e., a bound on the universe of discourse, searches for an in-
stance, i.e., a valuation to the relations in the formula such
that it evaluates to true. The analyzer translates an Alloy
formula (for the given scope) to a propositional formula and
finds an instance using an off-the-shelf SAT solver. The use
of an enumerating solver enables systematic test generation.
We have developed a prototype based on the AHEAD
theory. The prototype uses the recently developed Kodkod
model finding engine of the Alloy Analyzer. We illustrate
our approach using a data structure product line. |
@inproceedings{Uzuncaova2007,
title = {A specification-based approach to testing software product lines},
address = {New York, NY, USA},
author = {Engin Uzuncaova and Daniel Garcia and Sarfraz Khurshid and Don S. Batory},
booktitle = {ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering},
editor = {Ivica Crnkovic and Antonia Bertolino},
note = {ST: Die Spezifikation der Produktlinie liegt in einer formalen Beschreibung vor (LTL)
Es wird ein Modelchecking-Verfahren durchgefuehrt um zu beweisen, dass die Spezifikation gilt.
Fazit: Keine explizite Ableitung von Testdaten, die Spezifikation muss formal vorliegen.
MR: Anhand von formalen Alloy-Spezifikationen von Invarianten und Constraints kann der Alloy Analyzer (SAT solver) automatisch alle passenden Testdaten generieren.
Nachteile: Die erwarteten Ergebnisse werden nicht betrachtet (oder?). Die Spezifikation wird als Annotationen in den Code eingebracht (hier als moderner Ansatz angesehen ähnlich JML). An der Wiederverwendung wird erst gearbeitet.
},
pages = {525--528},
publisher = {ACM},
url = {http://doi.acm.org/10.1145/1287624.1287701},
year = {2007},
description = {Computer Science Bibliography Collection},
abstract = {This paper presents a specification-based approach for sys-
tematic testing of products from a software product line.
Our approach uses specifications given as formulas in Alloy,
a first-order logic based on relations. Alloy formulas can
be checked for satisfiability using the Alloy Analyzer. The
fully automatic analyzer, given an Alloy formula and a scope,
i.e., a bound on the universe of discourse, searches for an in-
stance, i.e., a valuation to the relations in the formula such
that it evaluates to true. The analyzer translates an Alloy
formula (for the given scope) to a propositional formula and
finds an instance using an off-the-shelf SAT solver. The use
of an enumerating solver enables systematic test generation.
We have developed a prototype based on the AHEAD
theory. The prototype uses the recently developed Kodkod
model finding engine of the Alloy Analyzer. We illustrate
our approach using a data structure product line.},
bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/sigsoft/fse2007.html#UzuncaovaGKB07}, bibdate = {2007-10-23}, isbn = {978-1-59593-811-4},
keywords = {AHEAD Alloy GenVoca generation line product specification-based testdata testing }
}
::