2018
Journal article
Open Access
A framework for quantitative modeling and analysis of highly (re)configurable systems
Ter Beek M., Legay A., Lluch Lafuente A., Vandin A.
security FOS: Computer and information sciences formal methods product line Software Software product lines probabilistic modeling statistical model checking Software Engineering (cs.SE) quantitative constraints Computer Science - Software Engineering
This paper presents our approach to the quantitative modeling and analysis of highly (re)configurable systems, like software product lines. Different combinations of the optional features of such systems give rise to combinatorially many individual system variants. We use a formal modeling language that allows us to model systems with probabilistic behavior, possibly subject to quantitative feature constraints, and able to dynamically install, remove or replace features. Our models are defined in the probabilistic feature-oriented language QFLan, a rich domain specific language (DSL) for systems with variability defined in terms of features. QFLan specifications are automatically encoded in terms of a process algebra whose operational behavior interacts with a store of constraints and with a semantics based on discrete-time Markov chains. Our analysis is based on statistical model checking, which allow us to scale to larger models with respect to precise probabilistic techniques. The analyses we can conduct range from the likelihood of specific behavior to the expected average cost of specific system variants. Our approach is supported by a novel Eclipse-based tool including state-of-the-art DSL utilities for QFLan as well as analysis plug-ins. We provide a number of case studies that have driven and validated the development of our framework.
Source: IEEE transactions on software engineering 46 (2018): 321–345. doi:10.1109/TSE.2018.2853726
Publisher: Institute of Electrical and Electronics Engineers], [New York,, Stati Uniti d'America
[1] A. Gruler, M. Leucker, and K. D. Scheidemann, “Modeling and Model Checking Software Product Lines,” in Proceedings of the 10th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'08), ser. LNCS, G. Barthe and F. S. de Boer, Eds., vol. 5051. Springer, 2008, pp. 113-131.
[2] M. Erwig and E. Walkingshaw, “The Choice Calculus: A Representation for Software Variation,” ACM Trans. Softw. Eng. Methodol., vol. 21, no. 1, 2011.
[3] A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin, “Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking,” IEEE Trans. Softw. Eng., vol. 39, no. 8, pp. 1069-1089, 2013.
[4] M. H. ter Beek and E. P. de Vink, “Using mCRL2 for the Analysis of Software Product Lines,” in Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE@ICSE'14), S. Gnesi and N. Plat, Eds. ACM, 2014, pp. 31-37.
[5] T. Thüm, S. Apel, C. Kästner, I. Schaefer, and G. Saake, “A Classification and Survey of Analysis Strategies for Software Product Lines,” ACM Comput. Surv., vol. 47, no. 1, 2014.
[6] M. Tribastone, “Behavioral Relations in a Process Algebra for Variants,” in Proceedings of the 18th International Software Product Line Conference (SPLC'14), S. Gnesi, A. Fantechi, P. Heymans, J. Rubin, and K. Czarnecki, Eds. ACM, 2014, pp. 82-91.
[7] M. H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti, “Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints,” J. Log. Algebr. Meth. Program., vol. 85, no. 2, pp. 287-315, 2016.
[8] M. Lochau, S. Mennicke, H. Baller, and L. Ribbeck, “Incremental model checking of delta-oriented software product lines,” J. Log. Algebr. Meth. Program., vol. 85, no. 1, pp. 245-267, 2016.
[9] A. S. Dimovski, A. S. Al-Sibahi, C. Brabrand, and A. Wa˛sowski, “Efficient family-based model checking via variability abstractions,” Int. J. Softw. Tools Technol. Transf., pp. 1-19, 2016.
[10] M. H. ter Beek, E. P. de Vink, and T. A. C. Willemse, “Family-Based Model Checking with mCRL2,” in Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17), ser. LNCS, M. Huisman and J. Rubin, Eds., vol. 10202. Springer, 2017, pp. 387-405.
[11] M. H. ter Beek, A. Lluch Lafuente, and M. Petrocchi, “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, 2013, pp. 10-17.
[12] M. H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin, “Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking,” in Proceedings of the 6th International Workshop on Formal Methods and Analysis for Software Product Line Engineering (FMSPLE'15), ser. EPTCS, J. M. Atlee and S. Gnesi, Eds., vol. 182, 2015, pp. 56-70.
[13] --, “Statistical analysis of probabilistic models of software product lines with quantitative constraints,” in Proceedings of the 19th International Software Product Line Conference (SPLC'15), D. C. Schmidt, Ed. ACM, 2015, pp. 11-15.
[14] --, “Statistical Model Checking for Product Lines,” in Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16), ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 9952. Springer, 2016, pp. 114-133.
[15] V. Saraswat and M. Rinard, “Concurrent Constraint Programming,” in Conference Record of the 17th Annual ACM Symposium on Principles of Programming Languages (POPL'90), F. E. Allen, Ed. ACM, 1990, pp. 232-245.
[16] M. G. Buscemi and U. Montanari, “CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements,” in Proceedings of the 16th European Symposium on Programming (ESOP'07), ser. LNCS, R. De Nicola, Ed., vol. 4421. Springer, 2007, pp. 18-32.
[17] L. Bortolussi, “Stochastic Concurrent Constraint Programming,” ENTCS, vol. 164, pp. 65-80, 2006.
[18] K. Czarnecki, S. Helsen, and U. W. Eisenecker, “Staged Configuration Using Feature Models,” in Proceedings of the 3rd International Software Product Lines Conference (SPLC'04), ser. LNCS, R. L. Nord, Ed., vol. 3154. Springer, 2004, pp. 266-283.
[19] J. Bürdek, S. Lity, M. Lochau, M. Berens, U. Goltz, and A. Schürr, “Staged Configuration of Dynamic Software Product Lines with Complex Binding Time Constraints,” in Proceedings of the 8th International Workshop on Variability Modelling of Software-intensive Systems (VaMoS'14), P. Collet, A. Wa˛sowski, and T. Weyer, Eds. ACM, 2014.
[20] M. Cordy, P.-Y. Schobbens, P. Heymans, and A. Legay, “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, 2013, pp. 472- 481.
[21] D. Benavides, S. Segura, and A. Ruiz-Cortés, “Automated Analysis of Feature Models 20 Years Later: a Literature Review,” Inf. Syst., vol. 35, no. 6, 2010.
[22] J. Mauro, M. Nieke, C. Seidl, and I. C. Yu, “Context Aware Reconfiguration in Software Product Lines,” in Proceedings of the 10th International Workshop on Variability Modelling of Software-intensive Systems (VaMoS '16), I. Schaefer, V. Alves, and E. S. de Almeida, Eds. ACM, 2016, pp. 41-48.
[23] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott, Eds., All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic, ser. LNCS, vol. 4350. Springer, 2007.
[24] S. Sebastio and A. Vandin, “MultiVeStA: Statistical Model Checking for Discrete Event Simulators,” in ValueTools, A. Horvath, P. Buchholz, V. Cortellessa, L. Muscariello, and M. S. Squillante, Eds. ACM, 2013, pp. 310-315.
[25] L. M. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), ser. LNCS, C. R. Ramakrishnan and J. Rehof, Eds., vol. 4963. Springer, 2008, pp. 337-340.
[26] C. Ghezzi and A. Molzam Sharifloo, “Model-based verification of quantitative non-functional properties for software product lines,” Inform. Softw. Technol., vol. 55, no. 3, pp. 508-524, 2013.
[27] M. Varshosaz and R. Khosravi, “Discrete Time Markov Chain Families: Modeling and Verification of Probabilistic Software Product Lines,” in Proceedings of the 17th International Software Product Line Conference (SPLC'13), vol. 2. ACM, 2013, pp. 34-41.
[28] C. Dubslaff, C. Baier, and S. Klüppelholz, “Probabilistic Model Checking for Feature-Oriented Systems,” in Transactions on AspectOriented Software Development XII, ser. LNCS, S. Chiba, E. Tanter, E. Ernst, and R. Hirschfeld, Eds., vol. 8989. Springer, 2015, pp. 180-220.
[29] G. N. Rodrigues, V. Alves, V. Nunes, A. Lanna, M. Cordy, P.- Y. Schobbens, A. Molzam Sharifloo, and A. Legay, “Modeling and Verification for Probabilistic Properties in Software Product Lines,” in Proceedings of the 16th International Symposium on HighAssurance Systems Engineering (HASE'15). IEEE, 2015, pp. 173-180.
[30] P. Chrszon, C. Dubslaff, S. Klüppelholz, and C. Baier, “FamilyBased Modeling and Analysis for Probabilistic Systems - Featuring PROFEAT,” in Proceedings of the 19th International Conference on Fundamental Approaches to Software Engineering (FASE'16), ser. LNCS, P. Stevens and A. Wa˛sowski, Eds., vol. 9633. Springer, 2016, pp. 287-304.
[31] M. Z. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of Probabilistic Real-Time Systems,” in CAV, ser. LNCS, G. Gopalakrishnan and S. Qadeer, Eds., vol. 6806. Springer, 2011, pp. 585-591.
[32] P. DeMaio, “Bike-sharing: History, Impacts, Models of Provision, and Future,” Journal of Public Transportation, vol. 12, no. 4, pp. 41- 56, 2009.
[33] P. Midgley, “Bicycle-Sharing Schemes: Enhancing Sustainable Mobility in Urban Areas,” Background Paper CSD19/2011/BP8, Commission on Sustainable Development, United Nations Department of Economic and Social Affairs, May 2011.
[34] M. Bartoletti, T. Cimoli, M. Murgia, A. S. Podda, and L. Pompianu, “A Contract-Oriented Middleware,” in Proceedings of the 12th International Conference on Formal Aspects of Component Software (FACS'15, ser. LNCS, C. Braga and P. C. Ölveczky, Eds., vol. 9539. Springer, 2015.
[35] S. Arora, A. Rathor, and M. V. P. Rao, “Statistical Model Checking of Opportunistic Network Protocols,” in Proceedings of the Asian Internet Engineering Conference (AINTEC'15). ACM, 2015, pp. 62- 68.
[36] L. Belzner, R. Hennicker, and M. Wirsing, “OnPlan: A Framework for Simulation-Based Online Planning,” in Proceedings of the 12th International Conference on Formal Aspects of Component Software (FACS'15, ser. LNCS, C. Braga and P. C. Ölveczky, Eds., vol. 9539. Springer, 2015, pp. 1-30.
[37] D. Pianini, S. Sebastio, and A. Vandin, “Distributed Statistical Analysis of Complex Systems Modeled Through a Chemical Metaphor,” in Proceedings of the International Conference on High Performance Computing & Simulation (HPCS'14). IEEE, 2014, pp. 416-423.
[38] S. Gilmore, M. Tribastone, and A. Vandin, “An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems,” in Proceedings of the 11th International Conference on Integrated Formal Methods (IFM'14), ser. LNCS, E. Albert and E. Sekerinski, Eds., vol. 8739. Springer, 2014, pp. 71-86.
[39] V. Ciancia, D. Latella, M. Massink, R. Paškauskas, and A. Vandin, “A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems,” in Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16), ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 9952. Springer, 2016, pp. 657-673.
[40] S. Sebastio, M. Amoretti, and A. Lluch Lafuente, “A Computational Field Framework for Collaborative Task Execution in Volunteer Clouds,” in Proceedings of the 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), G. Engels and N. Bencomo, Eds. ACM, 2014, pp. 105-114.
[41] L. Belzner, R. De Nicola, A. Vandin, and M. Wirsing, “Reasoning (on) Service Component Ensembles in Re- writing Logic,” in Specification, Algebra, and Software , ser. LNCS, S. Iida, J. Meseguer, and K. Ogata, Eds., vol. 8373. Springer, 2014, pp. 188-211.
[42] A. Legay, B. Delahaye, and S. Bensalem, “Statistical Model Checking: An Overview,” in Proceedings of the 1st International Conference on Runtime Verification (RV'10) , ser. LNCS, H. Barringer, Y. Falcone, B. Finkbeiner, K. Havelund, I. Lee, G. J. Pace, G. Rosu, O. Sokolsky, and N. Tillmann, Eds., vol. 6418. Springer, 2010, pp. 122-135.
[43] K. G. Larsen and A. Legay, “Statistical model checking: Past, present, and future,” in Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'14), ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 8802. Springer, 2014, pp. 135-142.
[44] G. Agha, J. Meseguer, and K. Sen, “PMaude: Rewrite-based Specification Language for Probabilistic Object Systems,” ENTCS, vol. 153, pp. 213-239, 2005.
[45] M. H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin, “Statistical Analysis of Probabilistic Models of Software Product Lines with Quantitative Constraints. Extended Version,” Tech. Rep. TR-QC-05-2015, June 2015. [Online]. Available: http://blog. inf.ed.ac.uk/quanticol/files/2015/07/18-Statistical-analysis.pdf
[46] P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi, “Formal Description of Variability in Product Families,” in Proceedings of the 15th International Software Product Lines Conference (SPLC'11), E. S. de Almeida, T. Kishi, C. Schwanninger, I. John, and K. Schmid, Eds. IEEE, 2011, pp. 130-139.
[47] M. H. ter Beek and E. P. de Vink, “Software Product Line Analysis with mCRL2,” in Proceedings of the 18th International Software Product Line Conference (SPLC'14), vol. 2. ACM, 2014, pp. 78-85.
[48] H. Beohar, M. Varshosaz, and M. R. Mousavi, “Basic behavioral models for software product lines: Expressiveness and testing preorders,” Sci. Comput. Program., vol. 123, pp. 42-60, 2016.
[49] 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,” in Proceedings of the 32nd International Conference on Software Engineering (ICSE'10). ACM, 2010, pp. 335-344.
[50] A. Fantechi and S. Gnesi, “Formal modeling for product families engineering,” in Proceedings of the 12th International Conference on Software Product Line Engineering (SPLC'08). IEEE, 2008, pp. 193- 202.
[51] R. Muschevici, J. Proença, and D. Clarke, “Feature Nets: behavioural modelling of software product lines,” Softw. Sys. Model., vol. 15, no. 4, pp. 1181-1206, 2016.
[52] A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens, “Formal semantics, modular specification, and symbolic verification of product-line behaviour,” Sci. Comput. Program., vol. 80, no. B, pp. 416-439, 2014.
[53] M. Plath and M. Ryan, “Feature integration using a feature construct,” Sci. Comput. Program., vol. 41, no. 1, pp. 53-84, 2001.
[54] S. Apel, A. von Rhein, P. Wendler, A. Größlinger, and D. Beyer, “Strategies for Product-line Verification: Case Studies and Experiments,” in Proceedings of the 35th International Conference on Software Engineering (ICSE'13). IEEE, 2013, pp. 482-491.
[55] A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay, “Symbolic model checking of software product lines,” in Proceedings of the 33rd International Conference on Software Engineering (ICSE'11). ACM, 2011, pp. 321-330.
[56] N. Macedo, J. Brunel, D. Chemouil, A. Cunha, and D. Kuperberg, “Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations,” in Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'16). ACM, 2016, pp. 373-383.
[57] J. Meinicke, C. Wong, C. Kästner, T. Thüm, and G. Saake, “On essential configuration complexity: measuring interactions in highly-configurable systems,” in Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE'16), D. Lo, S. Apel, and S. Khurshid, Eds. ACM, 2016, pp. 483-494.
[58] H. Sabouri, M. M. Jaghoori, F. S. de Boer, and R. Khosravi, “Scheduling and Analysis of Real-Time Software Families,” in Proceedings of the 36th Annual IEEE Computer Software and Applications Conference (COMPSAC'12), X. Bai, F. Belli, E. Bertino, C. K. Chang, A. Elçi, C. C. Seceleanu, H. Xie, and M. Zulkernine, Eds. IEEE, 2012, pp. 680-689.
[59] B. Schneier, 1999. [Online]. Available: https://www.schneier. com/academic/archives/1999/12/attack_trees.html
[60] W. Lv and W. Li, “Space Based Information System Security Risk Evaluation Based on Improved Attack Trees,” in Proceedings of the 3rd International Conference on Multimedia Information Networking and Security (MINES'11). IEEE, 2011, pp. 480-483.
[61] M. Cordy, A. Classen, P. Heymans, A. Legay, and P.-Y. Schobbens, “Model checking adaptive software with featured transition systems,” in Assurances for Self-Adaptive Systems: Principles, Models, and Techniques, ser. LNCS, J. Cámara, R. de Lemos, C. Ghezzi, and A. Lopes, Eds. Springer, 2013, vol. 7740, pp. 1-29.
[62] R. Bruni, A. Corradini, F. Gadducci, A. Lluch Lafuente, and A. Vandin, “A Conceptual Framework for Adaptation,” in Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering (FASE'12), ser. LNCS, J. de Lara and A. Zisman, Eds., vol. 7212. Springer, 2012, pp. 240-254.
[63] K. G. Larsen and B. Thomsen, “A Modal Process Logic,” in Proceedings of the 3rd Symposium on Logic in Computer Science (LICS'88). IEEE, 1988, pp. 203-210.
[64] D. Fischbein, S. Uchitel, and V. A. Braberman, “A foundation for behavioural conformance in software product line architectures,” in Proceedings of the ISSTA Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA'06), R. M. Hierons and H. Muccini, Eds. ACM, 2006, pp. 39-48.
[65] M. H. ter Beek, F. Damiani, S. Gnesi, F. Mazzanti, and L. Paolini, “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), ser. LNCS, R. Calinescu and B. Rumpe, Eds., vol. 9276. Springer, 2015, pp. 344-359.
[66] K. Lauenroth, K. Pohl, and S. Töhning, “Model Checking of Domain Artifacts in Product Line Engineering,” in Proceedings of the 24th International Conference on Automated Software Engineering (ASE'09). IEEE, 2009, pp. 269-280.
[67] K. G. Larsen, U. Nyman, and A. Wa˛sowski, “Modal I/O Automata for Interface and Product Line Theories,” in Proceedings of the 16th European Symposium on Programming (ESOP'07), ser. LNCS, R. De Nicola, Ed., vol. 4421. Springer, 2007, pp. 64-79.
[68] M. Leucker and D. Thoma, “A Formal Approach to Software Product Families,” in Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'12), Part I, ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 7609. Springer, 2012, pp. 131-145.
[69] D. Clarke, M. Helvensteijn, and I. Schaefer, “Abstract Delta Modeling,” ACM SIGPLAN Not., vol. 46, no. 2, pp. 13-22, Oct 2010.
[70] H. Zhang, H. Zou, F. Yang, and R. Lin, “Modeling and Analysis of Behavioral Variability in Product Lines,” J. Inf. Comput. Sci, vol. 9, no. 12, pp. 3589-3600, 2012.
[71] A. Gondal, M. Poppleton, and M. Butler, “Composing Event-B Specifications - Case-Study Experience,” in Proceedings of the 10th International Conference on Software Composition (SC'11), ser. LNCS, S. Apel and E. K. Jackson, Eds., vol. 6708. Springer, 2011, pp. 100-115.
[72] J.-V. Millo, S. Ramesh, S. N. Krishna, and G. K. Narwane, “Compositional Verification of Software Product Lines,” in Proceedings of the 10th International Conference on Integrated Formal Methods (IFM'13), ser. LNCS, E. B. Johnsen and L. Petre, Eds., vol. 7940. Springer, 2013, pp. 109-123.
[73] M. Kowal, I. Schaefer, and M. Tribastone, “Family-based performance analysis of variant-rich software systems,” in Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE'14), ser. LNCS, S. Gnesi and A. Rensink, Eds., vol. 8411. Springer, 2014, pp. 94-108.
[74] M. Kowal, M. Tschaikowski, M. Tribastone, and I. Schaefer, “Scaling Size and Parameter Spaces in Variability-aware Software Performance Models,” in Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE'15), ser. LNI, M. B. Cohen, L. Grunske, and M. Whalen, Eds., vol. 252. IEEE, 2015, pp. 407-417.
[75] S. Soleimanifard, D. Gurov, and M. Huisman, “ProMoVer: Modular Verification of Temporal Safety Properties,” in Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM'11, ser. LNCS, G. Barthe, A. Pardo, and G. Schneider, Eds., vol. 7041. Springer, 2011, pp. 366-381.
[76] I. Schaefer, D. Gurov, and S. Soleimanifard, “Compositional Algorithmic Verification of Software Product Lines,” in Revised Papers of the 9th International Symposium on Formal Methods for Components and Objects (FMCO'10), ser. LNCS, B. K. Aichernig, F. S. de Boer, and M. M. Bonsangue, Eds., vol. 6957. Springer, 2012, pp. 184- 203.
[77] S. Apel, H. Speidel, P. Wendler, A. von Rhein, and D. Beyer, “Detection of feature interactions using feature-aware verification,” in Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11). IEEE, 2011, pp. 372-375.
[78] W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda, “Model Checking Programs,” Autom. Softw. Eng., vol. 10, no. 2, pp. 203- 232, 2003.
[79] D. Beyer and M. E. Keremoglu, “CPAchecker: A Tool for Configurable Software Verification,” in Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11) , ser. LNCS, G. Gopalakrishnan and S. Qadeer, Eds., vol. 6806. Springer, 2011, pp. 184-190.
[80] M. Cordy, A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay, “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, 2013, pp. 141-146.
[81] A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens, “Model checking software product lines with SNIP,” Int. J. Softw. Tools Technol. Transf., vol. 14, no. 5, pp. 589-612, 2012.
[82] A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, “NuSMV: A New Symbolic Model Verifier,” in Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99) , ser. LNCS, N. Halbwachs and D. A. Peled, Eds., vol. 1633. Springer, 1999, pp. 495-499.
[83] M. H. ter Beek, F. Mazzanti, and A. Sulova, “VMC: A Tool for Product Variability Analysis,” in Proceedings of the 18th International Symposium on Formal Methods (FM'12), ser. LNCS, D. Giannakopoulou and D. Méry, Eds., vol. 7436. Springer, 2012, pp. 450-454.
[84] M. H. ter Beek and F. Mazzanti, “VMC: Recent Advances and Challenges Ahead,” in Proceedings of the 18th International Software Product Line Conference (SPLC'14), vol. 2. ACM, 2014, pp. 70-77.
[85] M. H. ter Beek and E. P. de Vink, “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) , ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 8802. Springer, 2014, pp. 368-385.
[86] S. Cranen, J. F. Groote, J. J. A. Keiren, F. P. M. Stappers, E. P. de Vink, W. Wesselink, and T. A. C. Willemse, “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), ser. LNCS, N. Piterman and S. A. Smolka, Eds., vol. 7795. Springer, 2013, pp. 199-213.
[87] J. F. Groote and M. R. Mousavi, Modeling and Analysis of Communicating Systems. The MIT Press, 2014.
[88] M. H. ter Beek, E. P. de Vink, and T. A. C. Willemse, “Towards a Feature mu-Calculus Targeting SPL Verification,” in Proceedings of the 7th International Workshop on Formal Methods and Analysis for Software Product Line Engineering (FMSPLE'16), ser. EPTCS, J. Rubin and T. Thüm, Eds., vol. 206, 2016, pp. 61-75.
[89] A. S. Dimovski, A. S. Al-Sibahi, C. Brabrand, and A. Wa˛sowski, “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), ser. LNCS, B. Fischer and J. Geldenhuys, Eds., vol. 9232. Springer, 2015, pp. 282-299.
[90] A. S. Dimovski and A. Wa˛sowski, “Variability-Specific Abstraction Refinement for Family-Based Model Checking,” in Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17), ser. LNCS, M. Huisman and J. Rubin, Eds., vol. 10202. Springer, 2017, pp. 406-423.
[91] T. Thüm, C. Kästner, F. Benduhn, J. Meinicke, G. Saake, and T. Leich, “FeatureIDE: An extensible framework for feature-oriented software development,” Sci. Comput. Program., vol. 79, pp. 70-85, 2014.
[92] A. David, P. G. Jensen, K. G. Larsen, M. Mikucionis, and J. H. Taankvist, “Uppaal Stratego,” in Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), ser. LNCS, C. Baier and C. Tinelli, Eds., vol. 9035. Springer, 2015, pp. 206-211.
[2] M. Erwig and E. Walkingshaw, “The Choice Calculus: A Representation for Software Variation,” ACM Trans. Softw. Eng. Methodol., vol. 21, no. 1, 2011.
[3] A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin, “Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking,” IEEE Trans. Softw. Eng., vol. 39, no. 8, pp. 1069-1089, 2013.
[4] M. H. ter Beek and E. P. de Vink, “Using mCRL2 for the Analysis of Software Product Lines,” in Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE@ICSE'14), S. Gnesi and N. Plat, Eds. ACM, 2014, pp. 31-37.
[5] T. Thüm, S. Apel, C. Kästner, I. Schaefer, and G. Saake, “A Classification and Survey of Analysis Strategies for Software Product Lines,” ACM Comput. Surv., vol. 47, no. 1, 2014.
[6] M. Tribastone, “Behavioral Relations in a Process Algebra for Variants,” in Proceedings of the 18th International Software Product Line Conference (SPLC'14), S. Gnesi, A. Fantechi, P. Heymans, J. Rubin, and K. Czarnecki, Eds. ACM, 2014, pp. 82-91.
[7] M. H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti, “Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints,” J. Log. Algebr. Meth. Program., vol. 85, no. 2, pp. 287-315, 2016.
[8] M. Lochau, S. Mennicke, H. Baller, and L. Ribbeck, “Incremental model checking of delta-oriented software product lines,” J. Log. Algebr. Meth. Program., vol. 85, no. 1, pp. 245-267, 2016.
[9] A. S. Dimovski, A. S. Al-Sibahi, C. Brabrand, and A. Wa˛sowski, “Efficient family-based model checking via variability abstractions,” Int. J. Softw. Tools Technol. Transf., pp. 1-19, 2016.
[10] M. H. ter Beek, E. P. de Vink, and T. A. C. Willemse, “Family-Based Model Checking with mCRL2,” in Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17), ser. LNCS, M. Huisman and J. Rubin, Eds., vol. 10202. Springer, 2017, pp. 387-405.
[11] M. H. ter Beek, A. Lluch Lafuente, and M. Petrocchi, “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, 2013, pp. 10-17.
[12] M. H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin, “Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking,” in Proceedings of the 6th International Workshop on Formal Methods and Analysis for Software Product Line Engineering (FMSPLE'15), ser. EPTCS, J. M. Atlee and S. Gnesi, Eds., vol. 182, 2015, pp. 56-70.
[13] --, “Statistical analysis of probabilistic models of software product lines with quantitative constraints,” in Proceedings of the 19th International Software Product Line Conference (SPLC'15), D. C. Schmidt, Ed. ACM, 2015, pp. 11-15.
[14] --, “Statistical Model Checking for Product Lines,” in Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16), ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 9952. Springer, 2016, pp. 114-133.
[15] V. Saraswat and M. Rinard, “Concurrent Constraint Programming,” in Conference Record of the 17th Annual ACM Symposium on Principles of Programming Languages (POPL'90), F. E. Allen, Ed. ACM, 1990, pp. 232-245.
[16] M. G. Buscemi and U. Montanari, “CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements,” in Proceedings of the 16th European Symposium on Programming (ESOP'07), ser. LNCS, R. De Nicola, Ed., vol. 4421. Springer, 2007, pp. 18-32.
[17] L. Bortolussi, “Stochastic Concurrent Constraint Programming,” ENTCS, vol. 164, pp. 65-80, 2006.
[18] K. Czarnecki, S. Helsen, and U. W. Eisenecker, “Staged Configuration Using Feature Models,” in Proceedings of the 3rd International Software Product Lines Conference (SPLC'04), ser. LNCS, R. L. Nord, Ed., vol. 3154. Springer, 2004, pp. 266-283.
[19] J. Bürdek, S. Lity, M. Lochau, M. Berens, U. Goltz, and A. Schürr, “Staged Configuration of Dynamic Software Product Lines with Complex Binding Time Constraints,” in Proceedings of the 8th International Workshop on Variability Modelling of Software-intensive Systems (VaMoS'14), P. Collet, A. Wa˛sowski, and T. Weyer, Eds. ACM, 2014.
[20] M. Cordy, P.-Y. Schobbens, P. Heymans, and A. Legay, “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, 2013, pp. 472- 481.
[21] D. Benavides, S. Segura, and A. Ruiz-Cortés, “Automated Analysis of Feature Models 20 Years Later: a Literature Review,” Inf. Syst., vol. 35, no. 6, 2010.
[22] J. Mauro, M. Nieke, C. Seidl, and I. C. Yu, “Context Aware Reconfiguration in Software Product Lines,” in Proceedings of the 10th International Workshop on Variability Modelling of Software-intensive Systems (VaMoS '16), I. Schaefer, V. Alves, and E. S. de Almeida, Eds. ACM, 2016, pp. 41-48.
[23] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott, Eds., All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic, ser. LNCS, vol. 4350. Springer, 2007.
[24] S. Sebastio and A. Vandin, “MultiVeStA: Statistical Model Checking for Discrete Event Simulators,” in ValueTools, A. Horvath, P. Buchholz, V. Cortellessa, L. Muscariello, and M. S. Squillante, Eds. ACM, 2013, pp. 310-315.
[25] L. M. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), ser. LNCS, C. R. Ramakrishnan and J. Rehof, Eds., vol. 4963. Springer, 2008, pp. 337-340.
[26] C. Ghezzi and A. Molzam Sharifloo, “Model-based verification of quantitative non-functional properties for software product lines,” Inform. Softw. Technol., vol. 55, no. 3, pp. 508-524, 2013.
[27] M. Varshosaz and R. Khosravi, “Discrete Time Markov Chain Families: Modeling and Verification of Probabilistic Software Product Lines,” in Proceedings of the 17th International Software Product Line Conference (SPLC'13), vol. 2. ACM, 2013, pp. 34-41.
[28] C. Dubslaff, C. Baier, and S. Klüppelholz, “Probabilistic Model Checking for Feature-Oriented Systems,” in Transactions on AspectOriented Software Development XII, ser. LNCS, S. Chiba, E. Tanter, E. Ernst, and R. Hirschfeld, Eds., vol. 8989. Springer, 2015, pp. 180-220.
[29] G. N. Rodrigues, V. Alves, V. Nunes, A. Lanna, M. Cordy, P.- Y. Schobbens, A. Molzam Sharifloo, and A. Legay, “Modeling and Verification for Probabilistic Properties in Software Product Lines,” in Proceedings of the 16th International Symposium on HighAssurance Systems Engineering (HASE'15). IEEE, 2015, pp. 173-180.
[30] P. Chrszon, C. Dubslaff, S. Klüppelholz, and C. Baier, “FamilyBased Modeling and Analysis for Probabilistic Systems - Featuring PROFEAT,” in Proceedings of the 19th International Conference on Fundamental Approaches to Software Engineering (FASE'16), ser. LNCS, P. Stevens and A. Wa˛sowski, Eds., vol. 9633. Springer, 2016, pp. 287-304.
[31] M. Z. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of Probabilistic Real-Time Systems,” in CAV, ser. LNCS, G. Gopalakrishnan and S. Qadeer, Eds., vol. 6806. Springer, 2011, pp. 585-591.
[32] P. DeMaio, “Bike-sharing: History, Impacts, Models of Provision, and Future,” Journal of Public Transportation, vol. 12, no. 4, pp. 41- 56, 2009.
[33] P. Midgley, “Bicycle-Sharing Schemes: Enhancing Sustainable Mobility in Urban Areas,” Background Paper CSD19/2011/BP8, Commission on Sustainable Development, United Nations Department of Economic and Social Affairs, May 2011.
[34] M. Bartoletti, T. Cimoli, M. Murgia, A. S. Podda, and L. Pompianu, “A Contract-Oriented Middleware,” in Proceedings of the 12th International Conference on Formal Aspects of Component Software (FACS'15, ser. LNCS, C. Braga and P. C. Ölveczky, Eds., vol. 9539. Springer, 2015.
[35] S. Arora, A. Rathor, and M. V. P. Rao, “Statistical Model Checking of Opportunistic Network Protocols,” in Proceedings of the Asian Internet Engineering Conference (AINTEC'15). ACM, 2015, pp. 62- 68.
[36] L. Belzner, R. Hennicker, and M. Wirsing, “OnPlan: A Framework for Simulation-Based Online Planning,” in Proceedings of the 12th International Conference on Formal Aspects of Component Software (FACS'15, ser. LNCS, C. Braga and P. C. Ölveczky, Eds., vol. 9539. Springer, 2015, pp. 1-30.
[37] D. Pianini, S. Sebastio, and A. Vandin, “Distributed Statistical Analysis of Complex Systems Modeled Through a Chemical Metaphor,” in Proceedings of the International Conference on High Performance Computing & Simulation (HPCS'14). IEEE, 2014, pp. 416-423.
[38] S. Gilmore, M. Tribastone, and A. Vandin, “An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems,” in Proceedings of the 11th International Conference on Integrated Formal Methods (IFM'14), ser. LNCS, E. Albert and E. Sekerinski, Eds., vol. 8739. Springer, 2014, pp. 71-86.
[39] V. Ciancia, D. Latella, M. Massink, R. Paškauskas, and A. Vandin, “A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems,” in Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16), ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 9952. Springer, 2016, pp. 657-673.
[40] S. Sebastio, M. Amoretti, and A. Lluch Lafuente, “A Computational Field Framework for Collaborative Task Execution in Volunteer Clouds,” in Proceedings of the 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), G. Engels and N. Bencomo, Eds. ACM, 2014, pp. 105-114.
[41] L. Belzner, R. De Nicola, A. Vandin, and M. Wirsing, “Reasoning (on) Service Component Ensembles in Re- writing Logic,” in Specification, Algebra, and Software , ser. LNCS, S. Iida, J. Meseguer, and K. Ogata, Eds., vol. 8373. Springer, 2014, pp. 188-211.
[42] A. Legay, B. Delahaye, and S. Bensalem, “Statistical Model Checking: An Overview,” in Proceedings of the 1st International Conference on Runtime Verification (RV'10) , ser. LNCS, H. Barringer, Y. Falcone, B. Finkbeiner, K. Havelund, I. Lee, G. J. Pace, G. Rosu, O. Sokolsky, and N. Tillmann, Eds., vol. 6418. Springer, 2010, pp. 122-135.
[43] K. G. Larsen and A. Legay, “Statistical model checking: Past, present, and future,” in Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'14), ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 8802. Springer, 2014, pp. 135-142.
[44] G. Agha, J. Meseguer, and K. Sen, “PMaude: Rewrite-based Specification Language for Probabilistic Object Systems,” ENTCS, vol. 153, pp. 213-239, 2005.
[45] M. H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin, “Statistical Analysis of Probabilistic Models of Software Product Lines with Quantitative Constraints. Extended Version,” Tech. Rep. TR-QC-05-2015, June 2015. [Online]. Available: http://blog. inf.ed.ac.uk/quanticol/files/2015/07/18-Statistical-analysis.pdf
[46] P. Asirelli, M. H. ter Beek, A. Fantechi, and S. Gnesi, “Formal Description of Variability in Product Families,” in Proceedings of the 15th International Software Product Lines Conference (SPLC'11), E. S. de Almeida, T. Kishi, C. Schwanninger, I. John, and K. Schmid, Eds. IEEE, 2011, pp. 130-139.
[47] M. H. ter Beek and E. P. de Vink, “Software Product Line Analysis with mCRL2,” in Proceedings of the 18th International Software Product Line Conference (SPLC'14), vol. 2. ACM, 2014, pp. 78-85.
[48] H. Beohar, M. Varshosaz, and M. R. Mousavi, “Basic behavioral models for software product lines: Expressiveness and testing preorders,” Sci. Comput. Program., vol. 123, pp. 42-60, 2016.
[49] 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,” in Proceedings of the 32nd International Conference on Software Engineering (ICSE'10). ACM, 2010, pp. 335-344.
[50] A. Fantechi and S. Gnesi, “Formal modeling for product families engineering,” in Proceedings of the 12th International Conference on Software Product Line Engineering (SPLC'08). IEEE, 2008, pp. 193- 202.
[51] R. Muschevici, J. Proença, and D. Clarke, “Feature Nets: behavioural modelling of software product lines,” Softw. Sys. Model., vol. 15, no. 4, pp. 1181-1206, 2016.
[52] A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens, “Formal semantics, modular specification, and symbolic verification of product-line behaviour,” Sci. Comput. Program., vol. 80, no. B, pp. 416-439, 2014.
[53] M. Plath and M. Ryan, “Feature integration using a feature construct,” Sci. Comput. Program., vol. 41, no. 1, pp. 53-84, 2001.
[54] S. Apel, A. von Rhein, P. Wendler, A. Größlinger, and D. Beyer, “Strategies for Product-line Verification: Case Studies and Experiments,” in Proceedings of the 35th International Conference on Software Engineering (ICSE'13). IEEE, 2013, pp. 482-491.
[55] A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay, “Symbolic model checking of software product lines,” in Proceedings of the 33rd International Conference on Software Engineering (ICSE'11). ACM, 2011, pp. 321-330.
[56] N. Macedo, J. Brunel, D. Chemouil, A. Cunha, and D. Kuperberg, “Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations,” in Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'16). ACM, 2016, pp. 373-383.
[57] J. Meinicke, C. Wong, C. Kästner, T. Thüm, and G. Saake, “On essential configuration complexity: measuring interactions in highly-configurable systems,” in Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE'16), D. Lo, S. Apel, and S. Khurshid, Eds. ACM, 2016, pp. 483-494.
[58] H. Sabouri, M. M. Jaghoori, F. S. de Boer, and R. Khosravi, “Scheduling and Analysis of Real-Time Software Families,” in Proceedings of the 36th Annual IEEE Computer Software and Applications Conference (COMPSAC'12), X. Bai, F. Belli, E. Bertino, C. K. Chang, A. Elçi, C. C. Seceleanu, H. Xie, and M. Zulkernine, Eds. IEEE, 2012, pp. 680-689.
[59] B. Schneier, 1999. [Online]. Available: https://www.schneier. com/academic/archives/1999/12/attack_trees.html
[60] W. Lv and W. Li, “Space Based Information System Security Risk Evaluation Based on Improved Attack Trees,” in Proceedings of the 3rd International Conference on Multimedia Information Networking and Security (MINES'11). IEEE, 2011, pp. 480-483.
[61] M. Cordy, A. Classen, P. Heymans, A. Legay, and P.-Y. Schobbens, “Model checking adaptive software with featured transition systems,” in Assurances for Self-Adaptive Systems: Principles, Models, and Techniques, ser. LNCS, J. Cámara, R. de Lemos, C. Ghezzi, and A. Lopes, Eds. Springer, 2013, vol. 7740, pp. 1-29.
[62] R. Bruni, A. Corradini, F. Gadducci, A. Lluch Lafuente, and A. Vandin, “A Conceptual Framework for Adaptation,” in Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering (FASE'12), ser. LNCS, J. de Lara and A. Zisman, Eds., vol. 7212. Springer, 2012, pp. 240-254.
[63] K. G. Larsen and B. Thomsen, “A Modal Process Logic,” in Proceedings of the 3rd Symposium on Logic in Computer Science (LICS'88). IEEE, 1988, pp. 203-210.
[64] D. Fischbein, S. Uchitel, and V. A. Braberman, “A foundation for behavioural conformance in software product line architectures,” in Proceedings of the ISSTA Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA'06), R. M. Hierons and H. Muccini, Eds. ACM, 2006, pp. 39-48.
[65] M. H. ter Beek, F. Damiani, S. Gnesi, F. Mazzanti, and L. Paolini, “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), ser. LNCS, R. Calinescu and B. Rumpe, Eds., vol. 9276. Springer, 2015, pp. 344-359.
[66] K. Lauenroth, K. Pohl, and S. Töhning, “Model Checking of Domain Artifacts in Product Line Engineering,” in Proceedings of the 24th International Conference on Automated Software Engineering (ASE'09). IEEE, 2009, pp. 269-280.
[67] K. G. Larsen, U. Nyman, and A. Wa˛sowski, “Modal I/O Automata for Interface and Product Line Theories,” in Proceedings of the 16th European Symposium on Programming (ESOP'07), ser. LNCS, R. De Nicola, Ed., vol. 4421. Springer, 2007, pp. 64-79.
[68] M. Leucker and D. Thoma, “A Formal Approach to Software Product Families,” in Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'12), Part I, ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 7609. Springer, 2012, pp. 131-145.
[69] D. Clarke, M. Helvensteijn, and I. Schaefer, “Abstract Delta Modeling,” ACM SIGPLAN Not., vol. 46, no. 2, pp. 13-22, Oct 2010.
[70] H. Zhang, H. Zou, F. Yang, and R. Lin, “Modeling and Analysis of Behavioral Variability in Product Lines,” J. Inf. Comput. Sci, vol. 9, no. 12, pp. 3589-3600, 2012.
[71] A. Gondal, M. Poppleton, and M. Butler, “Composing Event-B Specifications - Case-Study Experience,” in Proceedings of the 10th International Conference on Software Composition (SC'11), ser. LNCS, S. Apel and E. K. Jackson, Eds., vol. 6708. Springer, 2011, pp. 100-115.
[72] J.-V. Millo, S. Ramesh, S. N. Krishna, and G. K. Narwane, “Compositional Verification of Software Product Lines,” in Proceedings of the 10th International Conference on Integrated Formal Methods (IFM'13), ser. LNCS, E. B. Johnsen and L. Petre, Eds., vol. 7940. Springer, 2013, pp. 109-123.
[73] M. Kowal, I. Schaefer, and M. Tribastone, “Family-based performance analysis of variant-rich software systems,” in Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE'14), ser. LNCS, S. Gnesi and A. Rensink, Eds., vol. 8411. Springer, 2014, pp. 94-108.
[74] M. Kowal, M. Tschaikowski, M. Tribastone, and I. Schaefer, “Scaling Size and Parameter Spaces in Variability-aware Software Performance Models,” in Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE'15), ser. LNI, M. B. Cohen, L. Grunske, and M. Whalen, Eds., vol. 252. IEEE, 2015, pp. 407-417.
[75] S. Soleimanifard, D. Gurov, and M. Huisman, “ProMoVer: Modular Verification of Temporal Safety Properties,” in Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM'11, ser. LNCS, G. Barthe, A. Pardo, and G. Schneider, Eds., vol. 7041. Springer, 2011, pp. 366-381.
[76] I. Schaefer, D. Gurov, and S. Soleimanifard, “Compositional Algorithmic Verification of Software Product Lines,” in Revised Papers of the 9th International Symposium on Formal Methods for Components and Objects (FMCO'10), ser. LNCS, B. K. Aichernig, F. S. de Boer, and M. M. Bonsangue, Eds., vol. 6957. Springer, 2012, pp. 184- 203.
[77] S. Apel, H. Speidel, P. Wendler, A. von Rhein, and D. Beyer, “Detection of feature interactions using feature-aware verification,” in Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11). IEEE, 2011, pp. 372-375.
[78] W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda, “Model Checking Programs,” Autom. Softw. Eng., vol. 10, no. 2, pp. 203- 232, 2003.
[79] D. Beyer and M. E. Keremoglu, “CPAchecker: A Tool for Configurable Software Verification,” in Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11) , ser. LNCS, G. Gopalakrishnan and S. Qadeer, Eds., vol. 6806. Springer, 2011, pp. 184-190.
[80] M. Cordy, A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay, “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, 2013, pp. 141-146.
[81] A. Classen, M. Cordy, P. Heymans, A. Legay, and P.-Y. Schobbens, “Model checking software product lines with SNIP,” Int. J. Softw. Tools Technol. Transf., vol. 14, no. 5, pp. 589-612, 2012.
[82] A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, “NuSMV: A New Symbolic Model Verifier,” in Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99) , ser. LNCS, N. Halbwachs and D. A. Peled, Eds., vol. 1633. Springer, 1999, pp. 495-499.
[83] M. H. ter Beek, F. Mazzanti, and A. Sulova, “VMC: A Tool for Product Variability Analysis,” in Proceedings of the 18th International Symposium on Formal Methods (FM'12), ser. LNCS, D. Giannakopoulou and D. Méry, Eds., vol. 7436. Springer, 2012, pp. 450-454.
[84] M. H. ter Beek and F. Mazzanti, “VMC: Recent Advances and Challenges Ahead,” in Proceedings of the 18th International Software Product Line Conference (SPLC'14), vol. 2. ACM, 2014, pp. 70-77.
[85] M. H. ter Beek and E. P. de Vink, “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) , ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 8802. Springer, 2014, pp. 368-385.
[86] S. Cranen, J. F. Groote, J. J. A. Keiren, F. P. M. Stappers, E. P. de Vink, W. Wesselink, and T. A. C. Willemse, “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), ser. LNCS, N. Piterman and S. A. Smolka, Eds., vol. 7795. Springer, 2013, pp. 199-213.
[87] J. F. Groote and M. R. Mousavi, Modeling and Analysis of Communicating Systems. The MIT Press, 2014.
[88] M. H. ter Beek, E. P. de Vink, and T. A. C. Willemse, “Towards a Feature mu-Calculus Targeting SPL Verification,” in Proceedings of the 7th International Workshop on Formal Methods and Analysis for Software Product Line Engineering (FMSPLE'16), ser. EPTCS, J. Rubin and T. Thüm, Eds., vol. 206, 2016, pp. 61-75.
[89] A. S. Dimovski, A. S. Al-Sibahi, C. Brabrand, and A. Wa˛sowski, “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), ser. LNCS, B. Fischer and J. Geldenhuys, Eds., vol. 9232. Springer, 2015, pp. 282-299.
[90] A. S. Dimovski and A. Wa˛sowski, “Variability-Specific Abstraction Refinement for Family-Based Model Checking,” in Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17), ser. LNCS, M. Huisman and J. Rubin, Eds., vol. 10202. Springer, 2017, pp. 406-423.
[91] T. Thüm, C. Kästner, F. Benduhn, J. Meinicke, G. Saake, and T. Leich, “FeatureIDE: An extensible framework for feature-oriented software development,” Sci. Comput. Program., vol. 79, pp. 70-85, 2014.
[92] A. David, P. G. Jensen, K. G. Larsen, M. Mikucionis, and J. H. Taankvist, “Uppaal Stratego,” in Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), ser. LNCS, C. Baier and C. Tinelli, Eds., vol. 9035. Springer, 2015, pp. 206-211.
Metrics
Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:391581,
title = {A framework for quantitative modeling and analysis of highly (re)configurable systems},
author = {Ter Beek M. and Legay A. and Lluch Lafuente A. and Vandin A.},
publisher = {Institute of Electrical and Electronics Engineers], [New York,, Stati Uniti d'America},
doi = {10.1109/tse.2018.2853726 and 10.48550/arxiv.1707.08411},
journal = {IEEE transactions on software engineering},
volume = {46},
pages = {321–345},
year = {2018}
}CNR authorsLaboratories
0000-0002-2930-6367
