Subscribe

Issue No.08 - Aug. (2013 vol.39)

pp: 1069-1089

Andreas Classen , University of Namur (FUNDP), Namur

Maxime Cordy , University of Namur (FUNDP), Namur

Pierre-Yves Schobbens , University of Namur (FUNDP), Namur

Patrick Heymans , University of Namur (FUNDP), Namur and INRIA Lille-Nord Europe, France

Axel Legay , IRISA/INRIA Rennes, France Université de Liège, Rennes Liège

Jean-Francois Raskin , Université Libre de Bruxelles (ULB), Brussels

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.86

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 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.

INDEX TERMS

Unified modeling language, Semantics, Software, Labeling, Automata, Quality assurance, software product lines, Formal methods, model checking, verification, variability, features

CITATION

Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, Jean-Francois Raskin, "Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking",

*IEEE Transactions on Software Engineering*, vol.39, no. 8, pp. 1069-1089, Aug. 2013, doi:10.1109/TSE.2012.86REFERENCES

- [1] http://www.info.fundp.ac.befts, 2011.
- [2] M. Acher, P. Collet, P. Lahire, and R. France, "Composing Feature Models,"
Proc. Second Int'l Conf. Software Language Eng., pp. 62-81, 2009.- [3] D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel, "Learning Operational Requirements from Goal Models,"
Proc. 31st Int'l Conf. Software Eng., pp. 265-275, 2009.- [4] S. Apel, W. Scholz, C. Lengauer, and C. Kästner, "Detecting Dependencies and Interactions in Feature-Oriented Design,"
Proc. 21st IEEE Int'l Symp. Software Reliability Eng., pp. 161-170, 2010.- [5] S. Apel, H. Speidel, P. Wendler, A. von Rhein, and D. Beyer, "Detection of Feature Interactions Using Feature-Aware Verification,"
Proc. 26th IEEE/ACM Int'l Conf. Automated Software Eng., pp. 372-375, 2011.- [6] P. Asirelli, M.H.T. Beek, A. Fantechi, and S. Gnesi, "A Logical Framework to Deal with Variability,"
Proc. Eighth Int'l Conf. Integrated Formal Methods, pp. 43-58, 2010.- [7] P. Asirelli, M.H. ter Beek, S. Gnesi, and A. Fantechi, "Deontic Logics for Modeling Behavioural Variability,"
Proc. Third Int'l Workshop Variability Modelling of Software-Intensive Systems, pp. 71-76, 2009.- [8] P. Asirelli, M.H. ter Beek, S. Gnesi, and A. Fantechi, "A Deontic Logical Framework for Modelling Product Families,"
Proc. Fourth Int'l Workshop Variability Modelling of Software-Intensive Systems, pp. 36-44, 2010.- [9] F. Bachmann, M. Goedicke, J.C.S. do Prado Leite, R.L. Nord, K. Pohl, B. Ramesh, and A. Vilbig, "A Meta-Model for Representing Variability in Product Family Development,"
Proc. Int'l Workshop Product Family Eng., pp. 66-80, 2003.- [10] C. Baier and J.-P. Katoen,
Principles of Model Checking. MIT Press, 2007.- [11] D.S. Batory, "Feature Models, Grammars, and Propositional Formulas,"
Proc. Ninth Int'l Software Product Line Conf., pp. 7-20, 2005.- [12] I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, "Efficient Detection of Vacuity in Temporal Model Checking,"
Formal Methods in System Design, vol. 18, no. 2, pp. 141-162, 2001.- [13] Q. Boucher, A. Classen, P. Heymans, A. Bourdoux, and L. Demonceau, "Tag and Prune: A Pragmatic Approach to Software Product Line Implementation,"
Proc. 25th IEEE/ACM Int'l Conf. Automated Software Eng., pp. 333-336, 2010.- [14] G. Bruns and P. Godefroid, "Model Checking with Multi-Valued Logics,"
Proc. Int'l Colloquium Automata, Languages, and Programming, pp. 281-293, 2004.- [15] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,"
ACM Computing Surveys, vol. 24, no. 3, pp. 293-318, 1992.- [16] M. Calder, M. Kolberg, E.H. Magill, and S. Reiff-Marganiec, "Feature Interaction: A Critical Review and Considered Forecast,"
Computer Networks, vol. 41, no. 1, pp. 115-141, 2003.- [17] M. Chechik, B. Devereux, S.M. Easterbrook, and A. Gurfinkel, "Multi-Valued Symbolic Model-Checking,"
ACM Trans. Software Eng. and Methodology, vol. 12, no. 4, pp. 371-408, 2003.- [18] M. Chechik, B. Devereux, and A. Gurfinkel, "Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using Spin,"
Proc. Eighth Int'l Workshop Model Checking of Software, pp. 16-36, 2001.- [19] E. Clarke, O. Grumberg, and D. Peled,
Model Checking. MIT Press, 1999.- [20] A. Classen, "Modelling with FTS: A Collection of Illustrative Examples," Technical Report P-CS-TR SPLMC-00000001, PReCISE Research Center, Univ. of Namur, 2010.
- [21] A. Classen, "Modelling and Model Checking Variability-Intensive Systems," PhD dissertation, PReCISE Research Centre, Faculty of Computer Science, Univ. of Namur (FUNDP), Oct. 2011.
- [22] A. Classen, Q. Boucher, and P. Heymans, "A Text-Based Approach to Feature Modelling: Syntax and Semantics of TVL,"
Science Computer Programming, vol. 76, no. 12, pp. 1130-1143, 2011.- [23] A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens, "Model Checking Software Product Lines with SNIP,"
Int'l J. Software Tools for Technology Transfer, vol. 14, no. 5, pp. 589-612, 2012.- [24] A. Classen, P. Heymans, and P.-Y. Schobbens, "What's in a Feature: A Requirements Engineering Perspective,"
Proc. 11th Int'l Conf. Fundamental Approaches to Software Eng., pp. 16-30, 2008.- [25] A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay, "Symbolic Model Checking of Software Product Lines,"
Proc. 33rd Int'l Conf. Software Eng., pp. 321-330, 2011.- [26] A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay, and J.-F. Raskin, "Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines,"
Proc. 32nd Int'l Conf. Software Eng., pp. 335-344, 2010.- [27] A. Classen, P. Heymans, T.T. Tun, and B. Nuseibeh, "Towards Safer Composition,"
Proc. 31st IEEE Int'l Conf. Software Eng., pp. 227-230, 2009.- [28] P.C. Clements and L. Northrop,
Software Product Lines: Practices and Patterns. Addison-Wesley, 2001.- [29] E.G. Coffman, M. Elphick, and A. Shoshani, "System Deadlocks,"
ACM Computing Surveys, vol. 3, pp. 67-78, June 1971.- [30] C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, "Memory-Efficient Algorithms for the Verification of Temporal Properties,"
Formal Methods Systems Design, vol. 1, nos. 2/3, pp. 275-288, 1992.- [31] K. Czarnecki and M. Antkiewicz, "Mapping Features to Models: A Template Approach Based on Superimposed Variants,"
Proc. Fourth Int'l Conf. Generative Programming and Component Eng., pp. 422-437, 2005.- [32] K. Czarnecki and K. Pietroszek, "Verifying Feature- Based Model Templates against Well-Formedness OCL Constraints,"
Proc. Fifth Int'l Conf. Generative Programming and Component Eng., pp. 211-220, 2006.- [33] M. De Wulf, L. Doyen, T.A. Henzinger, and J.-F. Raskin, "Antichains: A New Algorithm for Checking Universality of Finite Automata,"
Proc. 18th Int'l Conf. Computer Aided Verification, pp. 17-30, 2006.- [34] C. Ebert and C. Jones, "Embedded Software: Facts, Figures, and Future,"
Computer, vol. 42, no. 4, pp. 42-52, Apr. 2009.- [35] A. Fantechi and S. Gnesi, "A Behavioural Model for Product Families,"
Proc. Sixth Joint Meeting European Software Eng. Conf. and ACM SIGSOFT Symp. Foundations of Software Eng., pp. 521-524, 2007.- [36] A. Fantechi and S. Gnesi, "Formal Modeling for Product Families Engineering,"
Proc. 12th Int'l Software Product Line Conf., pp. 193-202, 2008.- [37] D. Fischbein, S. Uchitel, and V. Braberman, "A Foundation for Behavioural Conformance in Software Product Line Architectures,"
Proc. ISSTA 2006 Workshop Role of Software Architecture for Testing and Analysis, pp. 39-48, 2006.- [38] P. Gastin and D. Oddoux, "Fast LTL to Büchi Automata Translation,"
Proc. 13th Int'l Conf. Computer Aided Verification, pp. 53-65, 2001.- [39] A. Gruler, M. Leucker, and K. Scheidemann, "Modeling and Model Checking Software Product Lines,"
Proc. 10th IFIP WG 6.1 Int'l Conf. Formal Methods for Open Object-Based Distributed Systems, pp. 113-131, 2008.- [40] A. Gurfinkel and M. Chechik, "Multi-Valued Model Checking via Classical Model Checking,"
Proc. Int'l Conf. Concurrency Theory, pp. 263-277, 2003.- [41] G.J. Holzmann,
The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004.- [42] D. Jackson, "Alloy: A Lightweight Object Modelling Notation,"
ACM Trans. Software and Eng, Methodology, vol. 11, no. 2, pp. 256-290, 2002.- [43] K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson, "Feature-Oriented Domain Analysis (FODA) Feasibility Study," Technical Report CMU/SEI-90-TR-21, SEI, CMU, Nov. 1990.
- [44] C. Kästner, S. Apel, and M. Kuhlemann, "Granularity in Software Product Lines,"
Proc. Int'l Conf. Software Eng., pp. 311-320, 2008.- [45] C. Kästner, S. Apel, and K. Ostermann, "The Road to Feature Modularity?"
Proc. Int'l Conf. Feature-Oriented Software Development, pp. 5:1-5:8, 2011.- [46] S. Katz, "A Superimposition Control Construct for Distributed Systems,"
ACM Trans. Programming Languages and Systems, vol. 15, pp. 337-356, Apr. 1993.- [47] C.H.P. Kim, E. Bodden, D.S. Batory, and S. Khurshid, "Reducing Configurations to Monitor in a Software Product Line,"
Proc. First Int'l Conf. Runtime Verification, pp. 285-299, 2010.- [48] J. Kramer, J. Magee, M. Sloman, and A. Lister, "CONIC: An Integrated Approach to Distributed Computer Control Systems,"
IEE Proc. Computers and Digital Techniques, vol. 130, no. 1, pp. 1-10, 1983.- [49] K.G. Larsen, "Modal Specifications,"
Automatic Verification Methods for Finite State Systems, pp. 232-246, 1989.- [50] K.G. Larsen, U. Nyman, and A. Wasowski, "Modal I/O Automata for Interface and Product Line Theories,"
Proc. 16th European Conf. Programming, pp. 64-79, 2007.- [51] K. Lauenroth, S. Töhning, and K. Pohl, "Model Checking of Domain Artifacts in Product Line Engineering,"
Proc. IEEE/ACM Int'l Conf. Automated Software Eng., pp. 269-280, 2009.- [52] H.C. Li, S. Krishnamurthi, and K. Fisler, "Verifying Cross-Cutting Features as Open Systems,"
Proc. Int'l Symp. Foundations of Software Eng., pp. 89-98, 2002.- [53] J. Liebig, S. Apel, C. Lengauer, C. Kästner, and M. Schulze, "An Analysis of the Variability in Forty Preprocessor-Based Software Product Lines,"
Proc. 32nd Int'l Conf. Software Eng., pp. 105-114, 2010.- [54] J. Liu, J. Dehlinger, and R. Lutz, "Safety Analysis of Software Product Lines Using State-Based Modeling,"
J. Systems and Software, vol. 80, no. 11, pp. 1879-1892, 2007.- [55] J. Magee and J. Kramer,
Concurrency: State Models & Java Programs. Wiley, 2006.- [56] M. Mendonca, A. Wasowski, and K. Czarnecki, "SAT-Based Analysis of Feature Models Is Easy,"
Proc. 13th Int'l Software Product Line Conf., pp. 231-240, 2009.- [57] R. Milner,
A Calculus of Communicating Systems. Springer, 1980.- [58] B. Morin, O. Barais, G. Nain, and J.-M. Jézéquel, "Taming Dynamically Adaptive Systems Using Models and Aspects,"
Proc. Int'l Conf. Software Eng., pp. 122-132, 2009.- [59] R. Muschevici, D. Clarke, and J.P. Ca, "Feature Petri Nets,"
Proc. First Int'l Workshop Formal Methods in Software Product Line Eng., Co-Located SPLC, 2010.- [60] C.H. Papadimitriou,
Computational Complexity. Addison-Wesley, 1994.- [61] D. Parnas, "On the Design and Development of Program Families,"
IEEE Trans. Software Eng., vol. 2, no. 1, pp. 1-9, Mar. 1976.- [62] D. Peled, "All from One, One for All: On Model Checking Using Representatives,"
Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 409-423, 1993.- [63] M. Plath and M. Ryan, "Feature Integration Using a Feature Construct,"
Scientific Computer Programming, vol. 41, no. 1, pp. 53-84, 2001.- [64] A. Pnueli, "The Temporal Logic of Programs,"
Proc. 18th Ann. Symp. Foundations of Computer Science, pp. 46-57, 1977.- [65] K. Pohl, G. Bockle, and F. van der Linden,
Software Product Line Engineering: Foundations, Principles and Techniques. Springer, 2005.- [66] P.-Y. Schobbens, P. Heymans, J.-C. Trigaux, and Y. Bontemps, "Feature Diagrams: A Survey and A Formal Semantics,"
Proc. IEEE 14th Int'l Requirements Eng. Conf., pp. 139-148, 2006.- [67] A.P. Sistla and E.M. Clarke, "The Complexity of Propositional Linear Temporal Logics,"
J. ACM, vol. 32, pp. 733-749, July 1985.- [68] A. Tarski, "A Lattice-Theoretical Fixpoint Theorem and Its Applications,"
Pacific J. Math., vol. 5, pp. 285-309, 1955.- [69] T.T. Tun, Q. Boucher, A. Classen, A. Hubaux, and P. Heymans, "Relating Requirements and Feature Configurations: A Systematic Approach,"
Proc. 13th Int'l Software Product Line Conf., pp. 201-210, 2009.- [70] W.M.P. van der Aalst, M. Dumas, F. Gottschalk, A.H.M. ter Hofstede, M.L. Rosa, and J. Mendling, "Correctness-Preserving Configuration of Business Process Models,"
Fundamental Approaches to Software Eng., pp. 46-61, 2008.- [71] M.Y. Vardi, "Branching versus Linear Time: Final Showdown,"
Proc. Seventh Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 1-22, 2001.- [72] M.Y. Vardi and P. Wolper, "An Automata-Theoretic Approach to Automatic Program Verification,"
Proc. First Symp. Logic in Computer Science, pp. 332-344, 1986.- [73] C. Wohlin, P. Runeson, M. Höst, M.C. Ohlsson, B. Regnell, and A. Wesslén,
Experimentation in Software Engineering: An Introduction. Kluwer, 2000.- [74] T. Ziadi, L. Hélouët, and J.-M. Jézéquel, "Towards a UML Profile for Software Product Lines,"
Proc. Int'l Workshop Product Family Eng., pp. 129-139, 2003. |