A specification-based approach to testing software product lines. Uzuncaova, E., Garcia, D., Khurshid, S., & Batory, D. S. In Crnkovic, I. & Bertolino, A., editors, 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, pages 525--528, New York, NY, USA, 2007. ACM. 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.
A specification-based approach to testing software product lines [link]Paper  abstract   bibtex   
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,
  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.},
  added-at = {2008-06-27T14:53:10.000+0200},
  address = {New York, NY, USA},
  author = {Uzuncaova, Engin and Garcia, Daniel and Khurshid, Sarfraz and Batory, Don S.},
  bibdate = {2007-10-23},
  bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/sigsoft/fse2007.html#UzuncaovaGKB07},
  biburl = {http://www.bibsonomy.org/bibtex/2295b43ca71fb9d71fe69cb755c7ae30d/ist_spl},
  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},
  description = {Computer Science Bibliography Collection},
  editor = {Crnkovic, Ivica and Bertolino, Antonia},
  interhash = {4895d2bad5e62a2a0d0ad1d3e5b0f05b},
  intrahash = {295b43ca71fb9d71fe69cb755c7ae30d},
  isbn = {978-1-59593-811-4},
  keywords = {line product AHEAD testdata testing Alloy GenVoca specification-based generation},
  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},
  privnote = {MR: gelesen},
  publisher = {ACM},
  timestamp = {2008-06-27T14:53:10.000+0200},
  title = {A specification-based approach to testing software product lines},
  url = {http://doi.acm.org/10.1145/1287624.1287701},
  year = 2007
}

Downloads: 0