BibSonomy publications for /user/ist_spl/AHEADFri Jun 27 14:53:10 CEST 2008New York, NY, USAESEC-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 engineeringST: 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. 525--528A specification-based approach to testing software product lines2007GenVoca generation testdata testing AHEAD product line specification-based Alloy 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.