@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
}

{"_id":"gzrkBLrfhm3bZo9bK","bibbaseid":"uzuncaova-garcia-khurshid-batory-aspecificationbasedapproachtotestingsoftwareproductlines-2007","downloads":0,"creationDate":"2015-12-10T07:19:23.797Z","title":"A specification-based approach to testing software product lines","author_short":["Uzuncaova, E.","Garcia, D.","Khurshid, S.","Batory, D. S."],"year":2007,"bibtype":"inproceedings","biburl":"http://www.bibsonomy.org/bib/author/Engin Erzin?items=1000","bibdata":{"bibtype":"inproceedings","type":"inproceedings","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":[{"propositions":[],"lastnames":["Uzuncaova"],"firstnames":["Engin"],"suffixes":[]},{"propositions":[],"lastnames":["Garcia"],"firstnames":["Daniel"],"suffixes":[]},{"propositions":[],"lastnames":["Khurshid"],"firstnames":["Sarfraz"],"suffixes":[]},{"propositions":[],"lastnames":["Batory"],"firstnames":["Don","S."],"suffixes":[]}],"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":[{"propositions":[],"lastnames":["Crnkovic"],"firstnames":["Ivica"],"suffixes":[]},{"propositions":[],"lastnames":["Bertolino"],"firstnames":["Antonia"],"suffixes":[]}],"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","bibtex":"@inproceedings{Uzuncaova2007,\n abstract = {This paper presents a specification-based approach for sys-\r\ntematic testing of products from a software product line.\r\nOur approach uses specifications given as formulas in Alloy,\r\na first-order logic based on relations. Alloy formulas can\r\nbe checked for satisfiability using the Alloy Analyzer. The\r\nfully automatic analyzer, given an Alloy formula and a scope,\r\ni.e., a bound on the universe of discourse, searches for an in-\r\nstance, i.e., a valuation to the relations in the formula such\r\nthat it evaluates to true. The analyzer translates an Alloy\r\nformula (for the given scope) to a propositional formula and\r\nfinds an instance using an off-the-shelf SAT solver. The use\r\nof an enumerating solver enables systematic test generation.\r\nWe have developed a prototype based on the AHEAD\r\ntheory. The prototype uses the recently developed Kodkod\r\nmodel finding engine of the Alloy Analyzer. We illustrate\r\nour approach using a data structure product line.},\n added-at = {2008-06-27T14:53:10.000+0200},\n address = {New York, NY, USA},\n author = {Uzuncaova, Engin and Garcia, Daniel and Khurshid, Sarfraz and Batory, Don S.},\n bibdate = {2007-10-23},\n bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/sigsoft/fse2007.html#UzuncaovaGKB07},\n biburl = {http://www.bibsonomy.org/bibtex/2295b43ca71fb9d71fe69cb755c7ae30d/ist_spl},\n 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},\n description = {Computer Science Bibliography Collection},\n editor = {Crnkovic, Ivica and Bertolino, Antonia},\n interhash = {4895d2bad5e62a2a0d0ad1d3e5b0f05b},\n intrahash = {295b43ca71fb9d71fe69cb755c7ae30d},\n isbn = {978-1-59593-811-4},\n keywords = {line product AHEAD testdata testing Alloy GenVoca specification-based generation},\n note = {ST: Die Spezifikation der Produktlinie liegt in einer formalen Beschreibung vor (LTL)\r\nEs wird ein Modelchecking-Verfahren durchgefuehrt um zu beweisen, dass die Spezifikation gilt. \r\nFazit: Keine explizite Ableitung von Testdaten, die Spezifikation muss formal vorliegen.\r\n\r\nMR: Anhand von formalen Alloy-Spezifikationen von Invarianten und Constraints kann der Alloy Analyzer (SAT solver) automatisch alle passenden Testdaten generieren. \r\nNachteile: 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.\r\n},\n pages = {525--528},\n privnote = {MR: gelesen},\n publisher = {ACM},\n timestamp = {2008-06-27T14:53:10.000+0200},\n title = {A specification-based approach to testing software product lines},\n url = {http://doi.acm.org/10.1145/1287624.1287701},\n year = 2007\n}\n\n","author_short":["Uzuncaova, E.","Garcia, D.","Khurshid, S.","Batory, D. S."],"editor_short":["Crnkovic, I.","Bertolino, A."],"key":"Uzuncaova2007","id":"Uzuncaova2007","bibbaseid":"uzuncaova-garcia-khurshid-batory-aspecificationbasedapproachtotestingsoftwareproductlines-2007","role":"author","urls":{"Paper":"http://doi.acm.org/10.1145/1287624.1287701"},"keyword":["line product AHEAD testdata testing Alloy GenVoca specification-based generation"],"downloads":0,"html":""},"search_terms":["specification","based","approach","testing","software","product","lines","uzuncaova","garcia","khurshid","batory"],"keywords":["line product ahead testdata testing alloy genvoca specification-based generation"],"authorIDs":[],"dataSources":["bJn8naASFAjyqsJYn"]}