Advertisement

QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems

  • Andrea Vandin
  • Maurice H. ter Beek
  • Axel Legay
  • Alberto Lluch Lafuente
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

QFLan offers modeling and analysis of highly reconfigurable systems, like product lines, which are characterized by combinatorially many system variants (or products) that can be obtained via different combinations of installed features. The tool offers a modern integrated development environment for the homonym probabilistic feature-oriented language. QFLan allows the specification of a family of products in terms of a feature model with quantitative attributes, which defines the valid feature combinations, and probabilistic behavior subject to quantitative constraints. The language’s behavioral part enables dynamic installation, removal and replacement of features. QFLan has a discrete-time Markov chain semantics, permitting quantitative analyses. Thanks to a seamless integration with the statistical model checker MultiVeStA, it allows for analyses like the likelihood of specific behavior or the expected average value of non-functional aspects related to feature attributes.

This is a preview of subscription content, log in to check access.

References

  1. 1.
    Apel, S., Batory, D.S., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37521-7CrossRefGoogle Scholar
  2. 2.
    ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Quantitative analysis of probabilistic models of software product lines with statistical model checking. In: FMSPLE 2015. EPTCS, vol. 182, pp. 56–70 (2015).  https://doi.org/10.4204/EPTCS.182.5
  3. 3.
    ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: SPLC 2015, pp. 11–15. ACM (2015).  https://doi.org/10.1145/2791060.2791087
  4. 4.
    ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114–133. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_8CrossRefGoogle Scholar
  5. 5.
    ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: A framework for quantitative modeling and analysis of highly (re)configurable systems. IEEE Transactions in Software Engineering (2018). http://arxiv.org/abs/1707.08411
  6. 6.
    ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450–454. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32759-9_36CrossRefGoogle Scholar
  7. 7.
    ter Beek, M.H., de Vink, E.P.: Using mCRL2 for the analysis of software product lines. In: FormaliSE 2014, pp. 31–37. ACM (2014).  https://doi.org/10.1145/2593489.2593493
  8. 8.
    ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Family-based model checking with mCRL2. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 387–405. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54494-5_23CrossRefGoogle Scholar
  9. 9.
    Benavides, D., Segura, S., Ruiz-Cortés, A.: Automated analysis of feature models 20 years later: a literature review. Inf. Syst. 35(6), 615–636 (2010).  https://doi.org/10.1016/j.is.2010.01.001CrossRefGoogle Scholar
  10. 10.
    Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: Family-based modeling and analysis for probabilistic systems – featuring ProFeat. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 287–304. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49665-7_17CrossRefGoogle Scholar
  11. 11.
    Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Asp. Comput. 30(1), 45–75 (2018).  https://doi.org/10.1007/s00165-017-0432-4MathSciNetCrossRefGoogle Scholar
  12. 12.
    Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf. 14(5), 589–612 (2012).  https://doi.org/10.1007/s10009-012-0234-1CrossRefGoogle Scholar
  13. 13.
    Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80(B), 416–439 (2014).  https://doi.org/10.1145/2499777.2499781CrossRefGoogle Scholar
  14. 14.
    Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: ICSE 2011, pp. 321–330. ACM (2011).  https://doi.org/10.1145/1985793.1985838
  15. 15.
    Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: ICSE 2010, pp. 335–344. ACM (2010).  https://doi.org/10.1145/1806799.1806850
  16. 16.
    Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71999-1CrossRefzbMATHGoogle Scholar
  17. 17.
    Cordy, M., Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: ProVeLines: a product line of verifiers for software product lines. In: SPLC 2013, pp. 141–146. ACM (2013).  https://doi.org/10.1145/2499777.2499781
  18. 18.
    Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A.: Beyond Boolean product-line model checking: dealing with feature attributes and multi-features. In: ICSE 2013, pp. 472–481. IEEE (2013).  https://doi.org/10.1109/ICSE.2013.6606593
  19. 19.
    Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wąsowski, A.: Efficient family-based model checking via variability abstractions. Int. J. Softw. Tools Technol. Transf. 19(5), 585–603 (2017).  https://doi.org/10.1007/s10009-016-0425-2CrossRefGoogle Scholar
  20. 20.
    Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wąsowski, A.: Family-based model checking without a family-based model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282–299. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23404-5_18CrossRefGoogle Scholar
  21. 21.
    Dimovski, A.S., Wąsowski, A.: Variability-specific abstraction refinement for family-based model checking. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 406–423. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54494-5_24CrossRefGoogle Scholar
  22. 22.
    Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113–131. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-68863-1_8CrossRefGoogle Scholar
  23. 23.
    Kowal, M., Schaefer, I., Tribastone, M.: Family-based performance analysis of variant-rich software systems. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 94–108. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54804-8_7CrossRefGoogle Scholar
  24. 24.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  25. 25.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16612-9_11CrossRefGoogle Scholar
  26. 26.
    Mauro, J., Nieke, M., Seidl, C., Yu, I.C.: Context aware reconfiguration in software product lines. In: VaMoS 2016, pp. 41–48. ACM (2016).  https://doi.org/10.1145/2866614.2866620
  27. 27.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  28. 28.
    Muschevici, R., Proença, J., Clarke, D.: Feature nets: behavioural modelling of software product lines. Softw. Syst. Model. 15(4), 1181–1206 (2016).  https://doi.org/10.1007/s10270-015-0475-zCrossRefGoogle Scholar
  29. 29.
    Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001).  https://doi.org/10.1016/S0167-6423(00)00018-6CrossRefzbMATHGoogle Scholar
  30. 30.
    Salay, R., Famelis, M., Rubin, J., Sandro, A.D., Chechik, M.: Lifting model transformations to product lines. In: ICSE 2014, pp. 117–128. ACM (2014).  https://doi.org/10.1145/2568225.2568267
  31. 31.
    Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: ValueTools 2013, pp. 310–315. ACM (2013)  https://doi.org/10.4108/icst.valuetools.2013.254377
  32. 32.
    Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6:1–6:45 (2014).  https://doi.org/10.1145/2580950CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Andrea Vandin
    • 1
  • Maurice H. ter Beek
    • 2
  • Axel Legay
    • 3
  • Alberto Lluch Lafuente
    • 1
  1. 1.DTULyngbyDenmark
  2. 2.ISTI–CNRPisaItaly
  3. 3.InriaRennesFrance

Personalised recommendations

Cite paper

Buy options