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.
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
{"_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"]}