Skip to main content
SpringerLink
Log in

Probabilistic Model Checking for Feature-Oriented Systems

  • Chapter
  • First Online:
Book cover Transactions on Aspect-Oriented Software Development XII

Part of the book series: Lecture Notes in Computer Science ((TAOSD,volume 8989))

Abstract

Within product lines, collections of several related products are defined through their commonalities in terms of features rather than specifying them individually one-by-one. In this paper we present a compositional framework for modeling dynamic product lines by a state-based formalism with both probabilistic and nondeterministic behaviors. Rules for feature changes in products made during runtime are formalized by a coordination component imposing constraints on possible feature activations and deactivations. Our framework supports large-scaled product lines described through multi-features, i.e., where products may involve multiple instances of a feature.

To establish temporal properties for products in a product line, verification techniques have to face a combinatorial blow-up that arises when reasoning about several feature combinations. This blow-up can be avoided by family-based approaches exploiting common feature behaviors. We adapt such approaches to our framework, allowing for a quantitative analysis in terms of probabilistic model checking to reason, e.g., about energy and memory consumption, monetary costs, or the reliability of products. Our framework can also be used to compute strategies how to trigger feature changes for optimizing quantitative objectives using probabilistic model-checking techniques.

We present a natural and conceptually simple translation of product lines into the input language of the prominent probabilistic model checker \(\textsc {Prism}\) and show feasibility of this translation within a case study on an energy-aware server platform product line comprising thousands of products. To cope with the arising complexity, we follow the family-based analysis scheme and apply symbolic methods for a compact state-space representation.

A preliminary version of this paper appeared at Modularity’14 [23].

The authors are supported by the DFG through the collaborative research centre HAEC (SFB 912), the cluster of excellence cfAED, Deutsche Telekom Stiftung, the ESF young researcher groups IMData (100098198) and SREX (100111037), the Graduiertenkolleg QuantLA (1763), the DFG/NWO-project ROCKS, and the EU-FP-7 grant MEALS (295261).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    For simplicity, we deal here with a single cost value for each guarded transition. Feature modules with multiple cost values will be considered in the case study of Sect. 5 and can be defined accordingly.

  2. 2.

    Activation and deactivation of network cards should not be confused with changing the network cards feature by plugging or unplugging cards.

References

  1. Apel, S., Hutchins, D.: A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. 32(5), 1–33 (2010)

    Article  Google Scholar 

  2. Apel, S., Janda, F., Trujillo, S., Kästner, C.: Model superimposition in software product lines. In: Paige, R.F. (ed.) ICMT 2009. LNCS, vol. 5563, pp. 4–19. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Baier, C., Dubslaff, C., Klein, J., Klüppelholz, S., Wunderlich, S.: Probabilistic model checking for energy-utility analysis. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. LNCS, vol. 8464, pp. 96–123. Springer, Heidelberg (2014)

    Google Scholar 

  4. Baier, C., Dubslaff, C., Klüppelholz, S., Daum, M., Klein, J., Märcker, S., Wunderlich, S.: Probabilistic model checking and non-standard multi-objective reasoning. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 1–16. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  5. Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  6. Baier, C., Kwiatkoswka, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125–155 (1998)

    Article  Google Scholar 

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

    Article  Google Scholar 

  8. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  9. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677–691 (1986)

    Article  MATH  Google Scholar 

  10. Chatterjee, K., Jurdzinski, M., Henzinger, T.: Quantitative simple stochastic parity games. In: Proceedings of the 15th ACM-SIAM Symposium on Discrete algorithms (SODA), pp. 121–130. SIAM (2004)

    Google Scholar 

  11. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 244–263 (1986)

    Article  MATH  Google Scholar 

  12. Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd Conference on Software Engineering (ICSE), pp. 321–330. ACM (2011)

    Google Scholar 

  13. 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: Proceedings of the 32rd Conference on Software Engineering (ICSE), pp. 335–344. ACM (2010)

    Google Scholar 

  14. Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley Professional, Reading (2001)

    Google Scholar 

  15. Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203–224 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  16. Cordy, M., Classen, A., Heymans, P., Legay, A., Schobbens, P.-Y.: Model checking adaptive software with featured transition systems. In: Cámara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds.) Assurances for Self-Adaptive Systems. LNCS, vol. 7740, pp. 1–29. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Cordy, M., Schobbens, P.-Y., Heymans, P., Legay, A.: Beyond boolean product-line model checking: dealing with feature attributes and multi-features. In: Proceedings of the 35rd Conference on Software Engineering (ICSE), pp. 472–481. IEEE Press (2013)

    Google Scholar 

  18. Czarnecki, K., Helsen, S., Eisenecker, U.W.: Formalizing cardinality-based feature models and their specialization. Softw. Process Improv. Pract. 10(1), 7–29 (2005)

    Article  Google Scholar 

  19. Damiani, F., Schaefer, I.: Dynamic delta-oriented programming. In: Proceedings of the 15th Software Product Line Conference (SPLC), vol. 2, pp. 34:1–34:8. ACM (2011)

    Google Scholar 

  20. de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, p. 66. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)

    Article  MATH  Google Scholar 

  22. Dinkelaker, T., Mitschke, R., Fetzer, K., Mezini, M.: A dynamic software product line approach using aspect models at runtime. In: Proceedings of the 1st Workshop on Composition and Variability (2010)

    Google Scholar 

  23. Dubslaff, C., Klüppelholz, S., Baier, C.: Probabilistic model checking for energy analysis in software product lines. In: Proceedings of the 13th Conference on Modularity (MODULARITY), pp. 169–180. ACM (2014)

    Google Scholar 

  24. Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)

    MATH  Google Scholar 

  25. Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  26. Fujita, M., McGeer, P., Yang, J.-Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst. Des. 10(2–3), 149–169 (1997)

    Article  Google Scholar 

  27. Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM 35(2), 96–107 (1992)

    Article  Google Scholar 

  28. Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Inf. Softw. Technol. 55(3), 508–524 (2013)

    Article  Google Scholar 

  29. Gomaa, H., Hussein, M.: Dynamic software reconfiguration in software product families. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 435–444. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  30. Hähnel, M., Döbel, B., Völp, M., Härtig, H.: eBond: energy saving in heterogeneous R.A.I.N. In: Proceedings of the 4th Conference on Future Energy Systems (e-Energy), pp. 193–202. ACM, New York (2013)

    Google Scholar 

  31. Hallsteinsen, S., Hinchey, M., Park, S., Schmid, K.: Dynamic software product lines. IEEE Comput. 41(4), 93–95 (2008)

    Article  Google Scholar 

  32. Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley, New York (1998)

    Book  Google Scholar 

  33. Hay, J.D., Atlee, J.M.: Composing features and resolving interactions. In: Proceedings of the 8th Symposium on Foundations of Software Engineering (SIGSOFT), pp. 110–119. ACM (2000)

    Google Scholar 

  34. Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  35. Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-oriented domain analysis (FODA) feasibility study. Technical report CMU/SEI-90-TR-21, Carnegie-Mellon University, November 1990

    Google Scholar 

  36. Katz, S.: A superimposition control construct for distributed systems. ACM Trans. Program. Lang. Syst. 15(2), 337–356 (1993)

    Article  Google Scholar 

  37. Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, London (1995)

    MATH  Google Scholar 

  38. Malik, S., Wang, A., Brayton, R., Sangiovanni-Vincentelli, A.: Logic verification using binary decision diagrams in a logic synthesis environment. In: Proceedings of the IEEE Conference on Computer-Aided Design (ICCAD), pp. 6–9 (1988)

    Google Scholar 

  39. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    Book  MATH  Google Scholar 

  40. Millo, J.-V., Ramesh, S., Krishna, S.N., Narwane, G.K.: Compositional verification of software product lines. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 109–123. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  41. Noorian, M., Bagheri, E., Du, W.: Non-functional properties in software product lines: a taxonomy for classification. In: Proceedings of the 24th Conference on Software Engineering & Knowledge Engineering (SEKE), pp. 663–667. Knowledge Systems Institute Graduate School (2012)

    Google Scholar 

  42. Papadopoulos, G.A., Arbab, F.: Coordination models and languages. Adv. Comput. 46, 329–400 (1998)

    Article  Google Scholar 

  43. Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)

    Article  MATH  Google Scholar 

  44. Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)

    MATH  Google Scholar 

  45. Rosenmüller, M., Siegmund, N., Apel, S., Saake, G.: Flexible feature binding in software product lines. Autom. Softw. Eng. 18(2), 163–197 (2011)

    Article  Google Scholar 

  46. Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the IEEE/ACM Conference on Computer-Aided Design (ICCAD), pp. 42–47. IEEE Computer Society (1993)

    Google Scholar 

  47. Schneider, J.-G., Lumpe, M., Nierstrasz, O.: Agent coordination via scripting languages. In: Omicini, A., Zambonelli, F., Klusch, M., Tolksdorf, R. (eds.) Coordination of Internet Agents: Models, Technologies, and Applications, pp. 153–175. Springer, New York (2001)

    Chapter  Google Scholar 

  48. Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)

    Google Scholar 

  49. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)

    MATH  MathSciNet  Google Scholar 

  50. Siegmund, N., Rosenmüller, M., Kästner, C., Giarrusso, P.G., Apel, S., Kolesnikov, S.S.: Scalable prediction of non-functional properties in software product lines: footprint and memory consumption. Inf. Softw. Technol. 55(3), 491–507 (2013)

    Article  Google Scholar 

  51. Siegmund, N., Rosenmüller, M., Kuhlemann, M., Kästner, C., Saake, G.: Measuring non-functional properties in software product line for product derivation. In: Proceedings of the 15th Asia-Pacific Software Engineering Conference (APSEC), pp. 187–194. IEEE (2008)

    Google Scholar 

  52. Varshosaz, M., Khosravi, R.: Discrete time Markov chain families: modeling and verification of probabilistic software product lines. In: Proceedings of the 17th Software Product Line Conference Co-located Workshops, pp. 34–41. ACM (2013)

    Google Scholar 

  53. von Rhein, A., Apel, S., Kästner, C., Thüm, T., Schaefer, I.: The PLA model: on the combination of product-line analyses. In: Proceedings of the 7th Workshop on Variability Modelling of Software-intensive Systems (VaMoS), pp. 14:1–14:8. ACM (2013)

    Google Scholar 

  54. White, J., Dougherty, B., Schmidt, D.C., Benavides, D.: Automated reasoning for multi-step feature model configuration problems. In: Proceedings of the 13th Software Product Line Conference (SPLC), pp. 11–20. ACM (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Computer Science, Technische Universität Dresden, Dresden, Germany

    Clemens Dubslaff, Christel Baier & Sascha Klüppelholz

Authors
  1. Clemens Dubslaff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christel Baier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sascha Klüppelholz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Clemens Dubslaff .

Editor information

Editors and Affiliations

  1. The University of Tokyo, Tokyo, Japan

    Shigeru Chiba

  2. University of Chile, Santiago, Chile

    Éric Tanter

  3. Google Aarhus, Aarhus, Denmark

    Erik Ernst

  4. Hasso Plattner Institute, Potsdam, Germany

    Robert Hirschfeld

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Dubslaff, C., Baier, C., Klüppelholz, S. (2015). Probabilistic Model Checking for Feature-Oriented Systems. In: Chiba, S., Tanter, É., Ernst, E., Hirschfeld, R. (eds) Transactions on Aspect-Oriented Software Development XII. Lecture Notes in Computer Science(), vol 8989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46734-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46734-3_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46733-6

  • Online ISBN: 978-3-662-46734-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation