2019
Conference article
Open Access
Static Analysis of Featured Transition Systems
Ter Beek M. H., Damiani F., Lienhardt M., F. Mazzanti F., Paolini L.
software product lines FORMAL METHODS SOFTWARE AND ITS ENGINEERING behavioural model [MATH]Mathematics [math] Featured transition systems static analysis Behavioural model Software product lines formal specification [SPI]Engineering Sciences [physics] [PHYS]Physics [physics] [INFO]Computer Science [cs] SPECIFICATION LANGUAGES Formal specification Static analysis featured transition systems
A Featured Transition System (FTS) is a formal behavioural model for software product lines, which represents the behaviour of all the products of an SPL in a single compact structure by associating transitions with features that condition their existence in products. In general, an FTS may contain featured transitions that are unreachable in any product (so called dead transitions) or, on the contrary, mandatorily present in all products for which their source state is reachable (so called false optional transitions), as well as states from which only for certain products progress is possible (so called hidden deadlocks). In this paper, we provide algorithms to analyse an FTS for such ambiguities and to transform an ambiguous FTS into an unambiguous FTS. The scope of our approach is twofold. First and foremost, an ambiguous model is typically undesired as it gives an unclear idea of the SPL. Second, an unambiguous FTS paves the way for efficient family-based model checking. We apply our approach to illustrative examples from the literature.
Source: 23rd International Systems and Software Product Line Conference (SPLC'19), pp. 39–51, Paris, France, 9-13 September 2019
Publisher: ACM Press, New York, USA
[1] Bowen Alpern and Fred B. Schneider. 1985. Defining liveness. Inf. Process. Lett. 4, 21 (1985), 181-185. https://doi.org/10.1016/0020-0190(85)90056-0
[2] Sven Apel, Don S. Batory, Christian Kästner, and Gunter Saake. 2013. FeatureOriented Software Product Lines: Concepts and Implementation. Springer. https: //doi.org/10.1007/978-3-642-37521-7
[3] Patrizia Asirelli, Maurice H. ter Beek, Alessandro Fantechi, and Stefania Gnesi. 2011. Formal Description of Variability in Product Families. In Proceedings of the 15th International Software Product Lines Conference (SPLC'11). IEEE, 130-139. https://doi.org/10.1109/SPLC.2011.34
[4] Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, and Sébastien Tabary. 2016. An Adaptive Parallel SAT Solver. In Proceedings of the 22nd International Conference onPrinciples and Practice of Constraint Programming (CP'16) (LNCS), M. Rueher (Ed.), Vol. 9892. Springer, 30-48. https://doi.org/10.1007/978-3-319- 44953-1_3
[5] Maurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti, and Luca Paolini. 2015. From Featured Transition Systems to Modal Transition Systems with Variability Constraints. In Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM'15) (LNCS), R. Calinescu and B. Rumpe (Eds.), Vol. 9276. Springer, 344-359. https://doi.org/10.1007/978-3- 319-22969-0_24
[6] Maurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti, and Luca Paolini. 2019. On the Expressiveness of Modal Transition Systems with Variability Constraints. Sci. Comput. Program. 169 (2019), 1-17. https://doi.org/ 10.1016/j.scico.2018.09.006
[7] Maurice H. ter Beek, Ferruccio Damiani, Michael Lienhardt, Franco Mazzanti, and Luca Paolini. 2019. Supplementary material for: “Static Analysis of Featured Transition Systems”. https://doi.org/10.5281/zenodo.2616646
[8] Maurice H. ter Beek and Erik P. de Vink. 2014. Towards Modular Verification of Software Product Lines with mCRL2. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'14) (LNCS), Tiziana Margaria and Bernhard Stefen (Eds.), Vol. 8802. Springer, 368-385. https://doi.org/10.1007/978-3-662-45234-9_26
[9] Maurice H. ter Beek and Erik P. de Vink. 2014. Using mCRL2 for the Analysis of Software Product Lines. In Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE'14). IEEE, 31-37. https://doi.org/10. 1145/2593489.2593493
[10] Maurice H. ter Beek, Erik P. de Vink, and Tim A. C. Willemse. 2017. FamilyBased Model Checking with mCRL2. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17) (LNCS), M. Huisman and J. Rubin (Eds.), Vol. 10202. Springer, 387-405. https://doi.org/ 10.1007/978-3-662-54494-5_23
[11] Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti. 2015. Using FMC for Family-based Analysis of Software Product Lines. In Proceedings of the 19th International Software Product Line Conference (SPLC'15). ACM, 432-439. https://doi.org/10.1145/2791060.2791118
[12] Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti. 2016. Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85, 2 (2016), 287-315. https://doi.org/10.1016/j.jlamp.2015.11.006
[13] Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti. 2019. States and Events in KandISTI: A Retrospective. In Models, Mindsets, Meta: The What, the How, and the Why Not?, T. Margaria, S. Graf, and K. G. Larsen (Eds.). LNCS, Vol. 11200. Springer, 110-128. https://doi.org/10.1007/978-3-030- 22348-9_9
[14] Maurice H. ter Beek, Stefania Gnesi, and Franco Mazzanti. 2015. From EU Projects to a Family of Model Checkers. In Software, Services and Systems, R. De Nicola and R. Hennicker (Eds.). LNCS, Vol. 8950. Springer, 312-328. https: //doi.org/10.1007/978-3-319-15545-6_20
[15] Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente, and Andrea Vandin. 2015. Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking. Electron. Proc. Theor. Comput. Sci. 182 (2015), 56-70. https://doi.org/10.4204/EPTCS.182.5
[16] Maurice H. ter Beek, Alberto Lluch Lafuente, and Marinella Petrocchi. 2013. Combining Declarative and Procedural Views in the Specification and Analysis of Product Families. In Proceedings of the 17th International Software Product Line Conference (SPLC'13), Vol. 2. ACM, 10-17. https://doi.org/10.1145/2499777. 2500722
[17] Maurice H. ter Beek and Franco Mazzanti. 2014. VMC: Recent Advances and Challenges Ahead. In Proceedings of the 18th International Software Product Line Conference (SPLC'14), Vol. 2. ACM, 70-77. https://doi.org/10.1145/2647908.2655969
[18] Maurice H. ter Beek, Franco Mazzanti, and Aldi Sulova. 2012. VMC: A Tool for Product Variability Analysis. In Proceedings of the 18th International Symposium on Formal Methods (FM'12) (LNCS), D. Giannakopoulou and D. Méry (Eds.), Vol. 7436. Springer, 450-454. https://doi.org/10.1007/978-3-642-32759-9_36
[19] Maurice H. ter Beek, Michel A. Reniers, and Erik P. de Vink. 2016. Supervisory Controller Synthesis for Product Lines Using CIF 3. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16) (LNCS), T. Margaria and B. Stefen (Eds.), Vol. 9952. Springer, 856-873. https://doi.org/10.1007/978-3-319- 47166-2_59
[20] David Benavides, Sergio Segura, and Antonio Ruiz-Cortés. 2010. Automated Analysis of Feature Models 20 Years Later: a Literature Review. Inf. Syst. 35, 6 (2010), 615-636. https://doi.org/10.1016/j.is.2010.01.001
[21] Harsh Beohar, Mahsa Varshosaz, and Mohammad Reza Mousavi. 2016. Basic behavioral models for software product lines: Expressiveness and testing preorders. Sci. Comput. Program. 123 (2016), 42-60. https://doi.org/10.1016/j.scico. 2015.06.005
[22] Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein. 2015. ν Z - An Optimizing SMT Solver. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15) (LNCS), C. Baier and C. Tinelli (Eds.), Vol. 9035. Springer, 194-199. https://doi.org/10.1007/978-3- 662-46681-0_14
[23] Eric Bodden, Társis Tolêdo, Márcio Ribeiro, Claus Brabrand, Paulo Borba, and Mira Mezini. 2013. SPLLIFT - Statically Analyzing Software Product Lines in Minutes Instead of Years. In Proceedings of the 34th Conference on Programming Language Design and Implementation (PLDI'13). ACM, 355-364. https://doi.org/ 10.1145/2491956.2491976
[24] Brian Chess and Jacob West. 2007. Secure Programming with Static Analysis. Addison-Wesley.
[25] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. 1986. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Sys. 8, 2 (1986), 244-263. https: //doi.org/10.1145/5397.5399
[26] Andreas Classen. 2010. Modelling with FTS: a Collection of Illustrative Examples. Technical Report P-CS-TR SPLMC-00000001. University of Namur.
[27] Andreas Classen. 2011. Modelling and Model Checking Variability-Intensive Systems. Ph.D. Dissertation. University of Namur.
[28] Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, and Pierre-Yves Schobbens. 2012. Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf. 14, 5 (2012), 589-612. https://doi.org/10.1007/s10009-012- 0234-1
[29] Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, and PierreYves Schobbens. 2014. Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, B (2014), 416-439. https://doi.org/10.1016/j.scico.2013.09.019
[30] Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, and Jean-François Raskin. 2013. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Softw. Eng. 39, 8 (2013), 1069-1089. https://doi.org/10. 1109/TSE.2012.86
[31] Andreas Classen, Pierre Heymans, Pierre-Yves Schobbens, and Axel Legay. 2011. Symbolic model checking of software product lines. In Proceedings of the 33rd International Conference on Software Engineering (ICSE'11). ACM, 321-330. https: //doi.org/10.1145/1985793.1985838
[32] Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay, and JeanFrançois Raskin. 2010. Model Checking Lots of Systems: Eficient Verification of Temporal Properties in Software Product Lines. In Proceedings of the 32nd International Conference on Software Engineering (ICSE'10). ACM, 335-344. https: //doi.org/10.1145/1806799.1806850
[33] Stephen A. Cook. 1971. The Complexity of Theorem-Proving Procedures. In Proceedings of the 3rd Annual Symposium on Theory of Computing (STOC'71). ACM, 151-158. https://doi.org/10.1145/800157.805047
[34] Maxime Cordy, Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, and Axel Legay. 2013. ProVeLines: A Product Line of Verifiers for Software Product Lines. In Proceedings of the 17th International Software Product Line Conference (SPLC'13), Vol. 2. ACM, 141-146. https://doi.org/10.1145/2499777.2499781
[35] Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay. 2012. Simulation-Based Abstractions for Software Product-Line Model Checking. In Proceedings of the 34th International Conference on Software Engineering (ICSE'12). IEEE, 672-682. https://doi.org/10.1109/ICSE. 2012.6227150
[36] Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay. 2013. Beyond Boolean Product-Line Model Checking: Dealing with Feature Attributes and Multi-features. In Proceedings of the 35th International Conference on Software Engineering (ICSE'13). IEEE, 472-481. https://doi.org/10.1109/ICSE.2013.6606593
[37] Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, and Tim A. C. Willemse. 2013. An Overview of the mCRL2 Toolset and Its Recent Advances. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13) (LNCS), N. Piterman and S. A. Smolka (Eds.), Vol. 7795. Springer, 199-213. https://doi.org/10.1007/978-3-642-36742-7_15
[38] Ferruccio Damiani, Michael Lienhardt, and Luca Paolini. 2017. A Formal Model for Multi SPLs. In Proceedings of the 7th International Conference on Fundamentals of Software Engineering (FSEN'17) (LNCS), M. Dastani and M. Sirjani (Eds.), Vol. 10522. Springer, 67-83. https://doi.org/10.1007/978-3-319-68972-2_5
[39] Ferruccio Damiani, Michael Lienhardt, and Luca Paolini. 2019. A formal model for Multi Software Product Lines. Sci. Comput. Program. 172 (2019), 203-231. https://doi.org/10.1016/j.scico.2018.11.005
[40] Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Eficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08) (LNCS), C. R. Ramakrishnan and J. Rehof (Eds.), Vol. 4963. Springer, 337-340. https://doi.org/ 10.1007/978-3-540-78800-3_24
[41] Rocco De Nicola and Frits W. Vaandrager. 1990. Action versus State based Logics for Transition Systems. In Semantics of Systems of Concurrent Processes: Proceedings of the LITP Spring School on Theoretical Computer Science (LNCS), I. Guessarian (Ed.), Vol. 469. Springer, 407-419. https://doi.org/10.1007/3-540- 53479-2_17
[42] Xavier Devroey, Gilles Perrouin, Axel Legay, Maxime Cordy, Pierre-Yves Schobbens, and Patrick Heymans. 2014. Coverage Criteria for Behavioural Testing of Software Product Lines. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'14) (LNCS), T. Margaria and B. Stefen (Eds.), Vol. 8802. Springer, 336-350. https://doi.org/10.1007/978-3-662-45234-9_24
[43] Xavier Devroey, Gilles Perrouin, Mike Papadakis, Axel Legay, Pierre-Yves Schobbens, and Patrick Heymans. 2016. Featured Model-based Mutation Analysis. In Proceedings of the 38th International Conference on Software Engineering (ICSE'16). ACM, 655-666. https://doi.org/10.1145/2884781.2884821
[44] Aleksandar S. Dimovski. 2018. Abstract Family-Based Model Checking Using Modal Featured Transition Systems: Preservation of CTL∗. In Proceedings of the 21st International Conference on Fundamental Approaches to Software Engineering (FASE'18) (LNCS), A. Russo and A. Schürr (Eds.), Vol. 10802. Springer, 301-318. https://doi.org/10.1007/978-3-319-89363-1_17
[45] Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej Wąsowski. 2017. Eficient family-based model checking via variability abstractions. Int. J. Softw. Tools Technol. Transf. 5, 19 (2017), 585-603. https://doi.org/10.1007/s10009-016-0425-2
[46] Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej Wąsowski. 2015. Family-Based Model Checking Without a Family-Based Model Checker. In Proceedings of the 22nd International SPIN Symposium on Model Checking of Software (SPIN'15) (LNCS), B. Fischer and J. Geldenhuys (Eds.), Vol. 9232. Springer, 282-299. https://doi.org/10.1007/978-3-319-23404-5_18
[47] Aleksandar S. Dimovski and Andrzej Wąsowski. 2017. Variability-Specific Abstraction Refinement for Family-Based Model Checking. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17) (LNCS), M. Huisman and J. Rubin (Eds.), Vol. 10202. Springer, 406-423. https://doi.org/10.1007/978-3-662-54494-5_24
[48] Marijn Heule, Matti Järvisalo, and Martin Suda. [n.d.]. The international SAT Competitions web page. https://www.satcompetition.org/. Accessed: 2019-03-22.
[49] Gerald Holl, Paul Grünbacher, and Rick Rabiser. 2012. A systematic review and an expert survey on capabilities supporting multi product lines. Inf. Softw. Technol. 54, 8 (2012), 828-852. https://doi.org/10.1016/j.infsof.2012.02.002
[50] Frank Hutter, Marius Lindauer, Adrian Balint, Sam Bayless, Holger Hoos, and Kevin Leyton-Brown. 2017. The Configurable SAT Solver Challenge (CSSC). Artifi. Intell. 243 (2017), 1-25. https://doi.org/10.1016/j.artint.2016.09.006
[51] Christian Kästner and Sven Apel. 2008. Type-checking Software Product Lines - A Formal Approach. In Proceedings of the 23rd International Conference on Automated Software Engineering (ASE'08). IEEE, 258-267. https://doi.org/10.1109/ASE.2008. 36
[52] Chang Hwan Peter Kim, Don S. Batory, and Sarfraz Khurshid. 2011. Reducing Combinatorics in Testing Product Lines. In Proceedings of the 10th International Conference on Aspect-Oriented Software Development (AOSD'11). ACM, 57-68. https://doi.org/10.1145/1960275.1960284
[53] Jan Křetínský. 2017. 30 Years of Modal Transition Systems: Survey of Extensions and Analysis. In Models, Algorithms, Logics and Tools, L. Aceto, G. Bacci, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare (Eds.). LNCS, Vol. 10460. Springer, 36-74. https://doi.org/10.1007/978-3-319-63121-9_3
[54] Kim Guldstrand Larsen and Bent Thomsen. 1988. A Modal Process Logic. In Proceedings of the 3rd Symposium on Logic in Computer Science (LICS'88). IEEE, 203-210. https://doi.org/10.1109/LICS.1988.5119
[55] Michael Lienhardt, Ferruccio Damiani, Simone Donetti, and Luca Paolini. 2018. Multi Software Product Lines in the Wild. In Proceedings of the 12th International Workshop on Variability Modelling of Software-Intensive Systems (VaMoS'18). ACM, 89-96. https://doi.org/10.1145/3168365.3170425
[56] Zohar Manna and Amir Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Springer. https://doi.org/10.1007/978-1-4612-4222-2
[57] Marcílio Mendonça, Andrzej Wąsowski, and Krzysztof Czarnecki. 2009. SATbased Analysis of Feature Models is Easy. In Proceedings of the 13th International Software Product Line Conference (SPLC'09). ACM, 231-240.
[58] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 2005. Principles of Program Analysis. Springer. https://doi.org/10.1007/978-3-662-03811-6
[59] Alexander von Rhein, Jörg Liebig, Andreas Janker, Christian Kästner, and Sven Apel. 2018. Variability-Aware Static Analysis at Scale: An Empirical Study. ACM Trans. Softw. Eng. Methodol. 27, 4 (2018), 18:1-18:33. https://doi.org/10.1145/ 3280986
[60] Thomas Thüm, Sven Apel, Christian Kästner, Ina Schaefer, and Gunter Saake. 2014. A Classification and Survey of Analysis Strategies for Software Product Lines. ACM Comput. Surv. 47, 1 (2014), 6:1-6:45. https://doi.org/10.1145/2580950
[61] Thomas Thüm, Christian Kästner, Fabian Benduhn, Jens Meinicke, Gunter Saake, and Thomas Leich. 2014. FeatureIDE: An extensible framework for featureoriented software development. Sci. Comput. Program. 79 (2014), 70-85. https: //doi.org/10.1016/j.scico.2012.06.002
[62] Mahsa Varshosaz, Harsh Beohar, and Mohammad Reza Mousavi. 2018. Basic behavioral models for software product lines: Revisited. Sci. Comput. Program. 168 (2018), 171-185. https://doi.org/10.1016/j.scico.2018.09.001
[2] Sven Apel, Don S. Batory, Christian Kästner, and Gunter Saake. 2013. FeatureOriented Software Product Lines: Concepts and Implementation. Springer. https: //doi.org/10.1007/978-3-642-37521-7
[3] Patrizia Asirelli, Maurice H. ter Beek, Alessandro Fantechi, and Stefania Gnesi. 2011. Formal Description of Variability in Product Families. In Proceedings of the 15th International Software Product Lines Conference (SPLC'11). IEEE, 130-139. https://doi.org/10.1109/SPLC.2011.34
[4] Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, and Sébastien Tabary. 2016. An Adaptive Parallel SAT Solver. In Proceedings of the 22nd International Conference onPrinciples and Practice of Constraint Programming (CP'16) (LNCS), M. Rueher (Ed.), Vol. 9892. Springer, 30-48. https://doi.org/10.1007/978-3-319- 44953-1_3
[5] Maurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti, and Luca Paolini. 2015. From Featured Transition Systems to Modal Transition Systems with Variability Constraints. In Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM'15) (LNCS), R. Calinescu and B. Rumpe (Eds.), Vol. 9276. Springer, 344-359. https://doi.org/10.1007/978-3- 319-22969-0_24
[6] Maurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti, and Luca Paolini. 2019. On the Expressiveness of Modal Transition Systems with Variability Constraints. Sci. Comput. Program. 169 (2019), 1-17. https://doi.org/ 10.1016/j.scico.2018.09.006
[7] Maurice H. ter Beek, Ferruccio Damiani, Michael Lienhardt, Franco Mazzanti, and Luca Paolini. 2019. Supplementary material for: “Static Analysis of Featured Transition Systems”. https://doi.org/10.5281/zenodo.2616646
[8] Maurice H. ter Beek and Erik P. de Vink. 2014. Towards Modular Verification of Software Product Lines with mCRL2. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'14) (LNCS), Tiziana Margaria and Bernhard Stefen (Eds.), Vol. 8802. Springer, 368-385. https://doi.org/10.1007/978-3-662-45234-9_26
[9] Maurice H. ter Beek and Erik P. de Vink. 2014. Using mCRL2 for the Analysis of Software Product Lines. In Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE'14). IEEE, 31-37. https://doi.org/10. 1145/2593489.2593493
[10] Maurice H. ter Beek, Erik P. de Vink, and Tim A. C. Willemse. 2017. FamilyBased Model Checking with mCRL2. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17) (LNCS), M. Huisman and J. Rubin (Eds.), Vol. 10202. Springer, 387-405. https://doi.org/ 10.1007/978-3-662-54494-5_23
[11] Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti. 2015. Using FMC for Family-based Analysis of Software Product Lines. In Proceedings of the 19th International Software Product Line Conference (SPLC'15). ACM, 432-439. https://doi.org/10.1145/2791060.2791118
[12] Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti. 2016. Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85, 2 (2016), 287-315. https://doi.org/10.1016/j.jlamp.2015.11.006
[13] Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti. 2019. States and Events in KandISTI: A Retrospective. In Models, Mindsets, Meta: The What, the How, and the Why Not?, T. Margaria, S. Graf, and K. G. Larsen (Eds.). LNCS, Vol. 11200. Springer, 110-128. https://doi.org/10.1007/978-3-030- 22348-9_9
[14] Maurice H. ter Beek, Stefania Gnesi, and Franco Mazzanti. 2015. From EU Projects to a Family of Model Checkers. In Software, Services and Systems, R. De Nicola and R. Hennicker (Eds.). LNCS, Vol. 8950. Springer, 312-328. https: //doi.org/10.1007/978-3-319-15545-6_20
[15] Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente, and Andrea Vandin. 2015. Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking. Electron. Proc. Theor. Comput. Sci. 182 (2015), 56-70. https://doi.org/10.4204/EPTCS.182.5
[16] Maurice H. ter Beek, Alberto Lluch Lafuente, and Marinella Petrocchi. 2013. Combining Declarative and Procedural Views in the Specification and Analysis of Product Families. In Proceedings of the 17th International Software Product Line Conference (SPLC'13), Vol. 2. ACM, 10-17. https://doi.org/10.1145/2499777. 2500722
[17] Maurice H. ter Beek and Franco Mazzanti. 2014. VMC: Recent Advances and Challenges Ahead. In Proceedings of the 18th International Software Product Line Conference (SPLC'14), Vol. 2. ACM, 70-77. https://doi.org/10.1145/2647908.2655969
[18] Maurice H. ter Beek, Franco Mazzanti, and Aldi Sulova. 2012. VMC: A Tool for Product Variability Analysis. In Proceedings of the 18th International Symposium on Formal Methods (FM'12) (LNCS), D. Giannakopoulou and D. Méry (Eds.), Vol. 7436. Springer, 450-454. https://doi.org/10.1007/978-3-642-32759-9_36
[19] Maurice H. ter Beek, Michel A. Reniers, and Erik P. de Vink. 2016. Supervisory Controller Synthesis for Product Lines Using CIF 3. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16) (LNCS), T. Margaria and B. Stefen (Eds.), Vol. 9952. Springer, 856-873. https://doi.org/10.1007/978-3-319- 47166-2_59
[20] David Benavides, Sergio Segura, and Antonio Ruiz-Cortés. 2010. Automated Analysis of Feature Models 20 Years Later: a Literature Review. Inf. Syst. 35, 6 (2010), 615-636. https://doi.org/10.1016/j.is.2010.01.001
[21] Harsh Beohar, Mahsa Varshosaz, and Mohammad Reza Mousavi. 2016. Basic behavioral models for software product lines: Expressiveness and testing preorders. Sci. Comput. Program. 123 (2016), 42-60. https://doi.org/10.1016/j.scico. 2015.06.005
[22] Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein. 2015. ν Z - An Optimizing SMT Solver. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15) (LNCS), C. Baier and C. Tinelli (Eds.), Vol. 9035. Springer, 194-199. https://doi.org/10.1007/978-3- 662-46681-0_14
[23] Eric Bodden, Társis Tolêdo, Márcio Ribeiro, Claus Brabrand, Paulo Borba, and Mira Mezini. 2013. SPLLIFT - Statically Analyzing Software Product Lines in Minutes Instead of Years. In Proceedings of the 34th Conference on Programming Language Design and Implementation (PLDI'13). ACM, 355-364. https://doi.org/ 10.1145/2491956.2491976
[24] Brian Chess and Jacob West. 2007. Secure Programming with Static Analysis. Addison-Wesley.
[25] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. 1986. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Sys. 8, 2 (1986), 244-263. https: //doi.org/10.1145/5397.5399
[26] Andreas Classen. 2010. Modelling with FTS: a Collection of Illustrative Examples. Technical Report P-CS-TR SPLMC-00000001. University of Namur.
[27] Andreas Classen. 2011. Modelling and Model Checking Variability-Intensive Systems. Ph.D. Dissertation. University of Namur.
[28] Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, and Pierre-Yves Schobbens. 2012. Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf. 14, 5 (2012), 589-612. https://doi.org/10.1007/s10009-012- 0234-1
[29] Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, and PierreYves Schobbens. 2014. Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, B (2014), 416-439. https://doi.org/10.1016/j.scico.2013.09.019
[30] Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, and Jean-François Raskin. 2013. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Softw. Eng. 39, 8 (2013), 1069-1089. https://doi.org/10. 1109/TSE.2012.86
[31] Andreas Classen, Pierre Heymans, Pierre-Yves Schobbens, and Axel Legay. 2011. Symbolic model checking of software product lines. In Proceedings of the 33rd International Conference on Software Engineering (ICSE'11). ACM, 321-330. https: //doi.org/10.1145/1985793.1985838
[32] Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay, and JeanFrançois Raskin. 2010. Model Checking Lots of Systems: Eficient Verification of Temporal Properties in Software Product Lines. In Proceedings of the 32nd International Conference on Software Engineering (ICSE'10). ACM, 335-344. https: //doi.org/10.1145/1806799.1806850
[33] Stephen A. Cook. 1971. The Complexity of Theorem-Proving Procedures. In Proceedings of the 3rd Annual Symposium on Theory of Computing (STOC'71). ACM, 151-158. https://doi.org/10.1145/800157.805047
[34] Maxime Cordy, Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, and Axel Legay. 2013. ProVeLines: A Product Line of Verifiers for Software Product Lines. In Proceedings of the 17th International Software Product Line Conference (SPLC'13), Vol. 2. ACM, 141-146. https://doi.org/10.1145/2499777.2499781
[35] Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay. 2012. Simulation-Based Abstractions for Software Product-Line Model Checking. In Proceedings of the 34th International Conference on Software Engineering (ICSE'12). IEEE, 672-682. https://doi.org/10.1109/ICSE. 2012.6227150
[36] Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay. 2013. Beyond Boolean Product-Line Model Checking: Dealing with Feature Attributes and Multi-features. In Proceedings of the 35th International Conference on Software Engineering (ICSE'13). IEEE, 472-481. https://doi.org/10.1109/ICSE.2013.6606593
[37] Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, and Tim A. C. Willemse. 2013. An Overview of the mCRL2 Toolset and Its Recent Advances. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13) (LNCS), N. Piterman and S. A. Smolka (Eds.), Vol. 7795. Springer, 199-213. https://doi.org/10.1007/978-3-642-36742-7_15
[38] Ferruccio Damiani, Michael Lienhardt, and Luca Paolini. 2017. A Formal Model for Multi SPLs. In Proceedings of the 7th International Conference on Fundamentals of Software Engineering (FSEN'17) (LNCS), M. Dastani and M. Sirjani (Eds.), Vol. 10522. Springer, 67-83. https://doi.org/10.1007/978-3-319-68972-2_5
[39] Ferruccio Damiani, Michael Lienhardt, and Luca Paolini. 2019. A formal model for Multi Software Product Lines. Sci. Comput. Program. 172 (2019), 203-231. https://doi.org/10.1016/j.scico.2018.11.005
[40] Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Eficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08) (LNCS), C. R. Ramakrishnan and J. Rehof (Eds.), Vol. 4963. Springer, 337-340. https://doi.org/ 10.1007/978-3-540-78800-3_24
[41] Rocco De Nicola and Frits W. Vaandrager. 1990. Action versus State based Logics for Transition Systems. In Semantics of Systems of Concurrent Processes: Proceedings of the LITP Spring School on Theoretical Computer Science (LNCS), I. Guessarian (Ed.), Vol. 469. Springer, 407-419. https://doi.org/10.1007/3-540- 53479-2_17
[42] Xavier Devroey, Gilles Perrouin, Axel Legay, Maxime Cordy, Pierre-Yves Schobbens, and Patrick Heymans. 2014. Coverage Criteria for Behavioural Testing of Software Product Lines. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'14) (LNCS), T. Margaria and B. Stefen (Eds.), Vol. 8802. Springer, 336-350. https://doi.org/10.1007/978-3-662-45234-9_24
[43] Xavier Devroey, Gilles Perrouin, Mike Papadakis, Axel Legay, Pierre-Yves Schobbens, and Patrick Heymans. 2016. Featured Model-based Mutation Analysis. In Proceedings of the 38th International Conference on Software Engineering (ICSE'16). ACM, 655-666. https://doi.org/10.1145/2884781.2884821
[44] Aleksandar S. Dimovski. 2018. Abstract Family-Based Model Checking Using Modal Featured Transition Systems: Preservation of CTL∗. In Proceedings of the 21st International Conference on Fundamental Approaches to Software Engineering (FASE'18) (LNCS), A. Russo and A. Schürr (Eds.), Vol. 10802. Springer, 301-318. https://doi.org/10.1007/978-3-319-89363-1_17
[45] Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej Wąsowski. 2017. Eficient family-based model checking via variability abstractions. Int. J. Softw. Tools Technol. Transf. 5, 19 (2017), 585-603. https://doi.org/10.1007/s10009-016-0425-2
[46] Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej Wąsowski. 2015. Family-Based Model Checking Without a Family-Based Model Checker. In Proceedings of the 22nd International SPIN Symposium on Model Checking of Software (SPIN'15) (LNCS), B. Fischer and J. Geldenhuys (Eds.), Vol. 9232. Springer, 282-299. https://doi.org/10.1007/978-3-319-23404-5_18
[47] Aleksandar S. Dimovski and Andrzej Wąsowski. 2017. Variability-Specific Abstraction Refinement for Family-Based Model Checking. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17) (LNCS), M. Huisman and J. Rubin (Eds.), Vol. 10202. Springer, 406-423. https://doi.org/10.1007/978-3-662-54494-5_24
[48] Marijn Heule, Matti Järvisalo, and Martin Suda. [n.d.]. The international SAT Competitions web page. https://www.satcompetition.org/. Accessed: 2019-03-22.
[49] Gerald Holl, Paul Grünbacher, and Rick Rabiser. 2012. A systematic review and an expert survey on capabilities supporting multi product lines. Inf. Softw. Technol. 54, 8 (2012), 828-852. https://doi.org/10.1016/j.infsof.2012.02.002
[50] Frank Hutter, Marius Lindauer, Adrian Balint, Sam Bayless, Holger Hoos, and Kevin Leyton-Brown. 2017. The Configurable SAT Solver Challenge (CSSC). Artifi. Intell. 243 (2017), 1-25. https://doi.org/10.1016/j.artint.2016.09.006
[51] Christian Kästner and Sven Apel. 2008. Type-checking Software Product Lines - A Formal Approach. In Proceedings of the 23rd International Conference on Automated Software Engineering (ASE'08). IEEE, 258-267. https://doi.org/10.1109/ASE.2008. 36
[52] Chang Hwan Peter Kim, Don S. Batory, and Sarfraz Khurshid. 2011. Reducing Combinatorics in Testing Product Lines. In Proceedings of the 10th International Conference on Aspect-Oriented Software Development (AOSD'11). ACM, 57-68. https://doi.org/10.1145/1960275.1960284
[53] Jan Křetínský. 2017. 30 Years of Modal Transition Systems: Survey of Extensions and Analysis. In Models, Algorithms, Logics and Tools, L. Aceto, G. Bacci, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare (Eds.). LNCS, Vol. 10460. Springer, 36-74. https://doi.org/10.1007/978-3-319-63121-9_3
[54] Kim Guldstrand Larsen and Bent Thomsen. 1988. A Modal Process Logic. In Proceedings of the 3rd Symposium on Logic in Computer Science (LICS'88). IEEE, 203-210. https://doi.org/10.1109/LICS.1988.5119
[55] Michael Lienhardt, Ferruccio Damiani, Simone Donetti, and Luca Paolini. 2018. Multi Software Product Lines in the Wild. In Proceedings of the 12th International Workshop on Variability Modelling of Software-Intensive Systems (VaMoS'18). ACM, 89-96. https://doi.org/10.1145/3168365.3170425
[56] Zohar Manna and Amir Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Springer. https://doi.org/10.1007/978-1-4612-4222-2
[57] Marcílio Mendonça, Andrzej Wąsowski, and Krzysztof Czarnecki. 2009. SATbased Analysis of Feature Models is Easy. In Proceedings of the 13th International Software Product Line Conference (SPLC'09). ACM, 231-240.
[58] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 2005. Principles of Program Analysis. Springer. https://doi.org/10.1007/978-3-662-03811-6
[59] Alexander von Rhein, Jörg Liebig, Andreas Janker, Christian Kästner, and Sven Apel. 2018. Variability-Aware Static Analysis at Scale: An Empirical Study. ACM Trans. Softw. Eng. Methodol. 27, 4 (2018), 18:1-18:33. https://doi.org/10.1145/ 3280986
[60] Thomas Thüm, Sven Apel, Christian Kästner, Ina Schaefer, and Gunter Saake. 2014. A Classification and Survey of Analysis Strategies for Software Product Lines. ACM Comput. Surv. 47, 1 (2014), 6:1-6:45. https://doi.org/10.1145/2580950
[61] Thomas Thüm, Christian Kästner, Fabian Benduhn, Jens Meinicke, Gunter Saake, and Thomas Leich. 2014. FeatureIDE: An extensible framework for featureoriented software development. Sci. Comput. Program. 79 (2014), 70-85. https: //doi.org/10.1016/j.scico.2012.06.002
[62] Mahsa Varshosaz, Harsh Beohar, and Mohammad Reza Mousavi. 2018. Basic behavioral models for software product lines: Revisited. Sci. Comput. Program. 168 (2018), 171-185. https://doi.org/10.1016/j.scico.2018.09.001
Metrics
Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:406688,
title = {Static Analysis of Featured Transition Systems},
author = {Ter Beek M. H. and Damiani F. and Lienhardt M. and F. Mazzanti F. and Paolini L.},
publisher = {ACM Press, New York, USA},
doi = {10.1145/3336294.3336295},
booktitle = {23rd International Systems and Software Product Line Conference (SPLC'19), pp. 39–51, Paris, France, 9-13 September 2019},
year = {2019}
}
0000-0003-4562-8777CNR ExploRA
ISTI Repository
DOIAlso available from
ISTI Repository
DOIAlso available from
hal.archives-ouvertes.fr
Archivio Istituzionale
dl.acm.org
Hyper Article en Ligne