The Community for Technology Leaders
Green Image
Issue No. 08 - Aug. (2013 vol. 39)
ISSN: 0098-5589
pp: 1069-1089
Axel Legay , IRISA/INRIA Rennes, France Université de Liège, Rennes Liège
Pierre-Yves Schobbens , University of Namur (FUNDP), Namur
Patrick Heymans , University of Namur (FUNDP), Namur and INRIA Lille-Nord Europe, France
Maxime Cordy , University of Namur (FUNDP), Namur
Jean-Francois Raskin , Université Libre de Bruxelles (ULB), Brussels
Andreas Classen , University of Namur (FUNDP), Namur
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.
Unified modeling language, Semantics, Software, Labeling, Automata, Quality assurance, software product lines, Formal methods, model checking, verification, variability, features
Axel Legay, Pierre-Yves Schobbens, Patrick Heymans, Maxime Cordy, Jean-Francois Raskin, Andreas Classen, "Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking", IEEE Transactions on Software Engineering, vol. 39, no. , pp. 1069-1089, Aug. 2013, doi:10.1109/TSE.2012.86
93 ms
(Ver )