Abstract
| Original language | English |
|---|---|
| Pages (from-to) | 1069-1089 |
| Number of pages | 21 |
| Journal | IEEE Transactions on Software Engineering |
| Volume | 39 |
| Issue number | 8 |
| DOIs | |
| Publication status | Published - 1 Jan 2013 |
Fingerprint
Cite this
}
Featured transition systems : Foundations for verifying variability-intensive systems and their application to LTL model checking. / Classen, A.; Cordy, M.; Schobbens, P.-Y.; Heymans, P.; Legay, A.; Raskin, J.-F.
In: IEEE Transactions on Software Engineering, Vol. 39, No. 8, 01.01.2013, p. 1069-1089.Research output: Contribution to journal › Article
TY - JOUR
T1 - Featured transition systems
T2 - Foundations for verifying variability-intensive systems and their application to LTL model checking
AU - Classen, A.
AU - Cordy, M.
AU - Schobbens, P.-Y.
AU - Heymans, P.
AU - Legay, A.
AU - Raskin, J.-F.
PY - 2013/1/1
Y1 - 2013/1/1
N2 - 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 linear time logic (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 behaviors of a variability-intensive system. The 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.
AB - 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 linear time logic (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 behaviors of a variability-intensive system. The 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.
UR - http://www.scopus.com/inward/record.url?scp=84883057503&partnerID=8YFLogxK
U2 - 10.1109/TSE.2012.86
DO - 10.1109/TSE.2012.86
M3 - Article
AN - SCOPUS:84883057503
VL - 39
SP - 1069
EP - 1089
JO - IEEE Transactions on Software Engineering
JF - IEEE Transactions on Software Engineering
SN - 0098-5589
IS - 8
ER -