Paper in IEEE Trans Software Eng (TSE)
Back in the summer of 2011 we submitted a paper to IEEE Transactions on Software Engineering (TSE). Since this was a regular submission, things went quite slow, but at last, we finally received the acceptance letter! On measures such as impact factor, TSE is consistently ranked as one of the top three Software Engineering journals, so we’re happy.
Here is the abstract:
The premise of variability-intensive systems, specifically in software product line engineering, is the ability to produce a large family of different systems efficiently. Many such systems are critical. Thorough quality assurance techniques are thus required. Unfortunately, most quality assurance techniques were not designed with variability in mind. They work for single systems, and are too costly to apply to the whole system family. In this paper, we propose an efficient automata-based approach to LTL model checking of variability-intensive systems.
We build on earlier work in which we proposed Featured Transitions Systems (FTSs), a compact mathematical model for representing the behaviours of a variability-intensive system. FTS model checking algorithms verify all products of a family at once and pinpoint those that are faulty. This paper complements our earlier work, covering important theoretical aspects such as expressiveness and parallel composition as well as more practical things like vacuity detection and our logic feature LTL. Furthermore, we provide an in-depth treatment of the FTS model checking algorithm. Finally, we present SNIP, a new model checker for variability-intensive systems. The benchmarks conducted with SNIP confirm the speedups reported previously.
You can download a preprint here.