A specification-based approach to testing software product lines

This paper presents a specification-based approach for systematic 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 instance, 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. Categories and Subject Descriptors: D.2.5 [Software Enginee...

• Type: Conference
• Year: 2007
• Where: SIGSOFT
• Authors: Engin Uzuncaova, Daniel Garcia, Sarfraz Khurshid, Don S. Batory
• Keywords: Alloy Analyzer, Alloy Formula, Off-the-shelf Sat Solver, SIGSOFT 2007, Software Engineering