Skip to main content
Top

2015 | OriginalPaper | Chapter

Probabilistic Model Checking for Feature-Oriented Systems

Authors : Clemens Dubslaff, Christel Baier, Sascha Klüppelholz

Published in: Transactions on Aspect-Oriented Software Development XII

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
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
Activation and deactivation of network cards should not be confused with changing the network cards feature by plugging or unplugging cards.
 
Literature
1.
go back to reference Apel, S., Hutchins, D.: A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. 32(5), 1–33 (2010)CrossRef Apel, S., Hutchins, D.: A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. 32(5), 1–33 (2010)CrossRef
2.
go back to reference 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) CrossRef 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) CrossRef
3.
go back to reference 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) 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)
4.
go back to reference 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) CrossRef 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) CrossRef
5.
go back to reference Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)MATH
6.
go back to reference Baier, C., Kwiatkoswka, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125–155 (1998)CrossRef Baier, C., Kwiatkoswka, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125–155 (1998)CrossRef
7.
go back to reference 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)CrossRef 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)CrossRef
8.
go back to reference 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) CrossRef 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) CrossRef
9.
go back to reference Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677–691 (1986)CrossRefMATH Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677–691 (1986)CrossRefMATH
10.
go back to reference 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) 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)
11.
go back to reference 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)CrossRefMATH 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)CrossRefMATH
12.
go back to reference 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) 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)
13.
go back to reference 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) 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)
14.
go back to reference Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley Professional, Reading (2001) Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley Professional, Reading (2001)
16.
go back to reference 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) CrossRef 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) CrossRef
17.
go back to reference 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) 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)
18.
go back to reference Czarnecki, K., Helsen, S., Eisenecker, U.W.: Formalizing cardinality-based feature models and their specialization. Softw. Process Improv. Pract. 10(1), 7–29 (2005)CrossRef Czarnecki, K., Helsen, S., Eisenecker, U.W.: Formalizing cardinality-based feature models and their specialization. Softw. Process Improv. Pract. 10(1), 7–29 (2005)CrossRef
19.
go back to reference 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) 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)
20.
go back to reference 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) CrossRef 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) CrossRef
21.
go back to reference de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)CrossRefMATH de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)CrossRefMATH
22.
go back to reference 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) 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)
23.
go back to reference 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) 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)
24.
go back to reference Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)MATH Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)MATH
25.
go back to reference 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) CrossRef 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) CrossRef
26.
go back to reference 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)CrossRef 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)CrossRef
27.
go back to reference Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM 35(2), 96–107 (1992)CrossRef Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM 35(2), 96–107 (1992)CrossRef
28.
go back to reference 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)CrossRef 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)CrossRef
29.
go back to reference 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) CrossRef 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) CrossRef
30.
go back to reference 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) 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)
31.
go back to reference Hallsteinsen, S., Hinchey, M., Park, S., Schmid, K.: Dynamic software product lines. IEEE Comput. 41(4), 93–95 (2008)CrossRef Hallsteinsen, S., Hinchey, M., Park, S., Schmid, K.: Dynamic software product lines. IEEE Comput. 41(4), 93–95 (2008)CrossRef
32.
go back to reference Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley, New York (1998)CrossRef Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley, New York (1998)CrossRef
33.
go back to reference 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) 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)
34.
go back to reference 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) CrossRef 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) CrossRef
35.
go back to reference 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 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
36.
go back to reference Katz, S.: A superimposition control construct for distributed systems. ACM Trans. Program. Lang. Syst. 15(2), 337–356 (1993)CrossRef Katz, S.: A superimposition control construct for distributed systems. ACM Trans. Program. Lang. Syst. 15(2), 337–356 (1993)CrossRef
37.
go back to reference Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, London (1995)MATH Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, London (1995)MATH
38.
go back to reference 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) 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)
39.
40.
go back to reference 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) CrossRef 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) CrossRef
41.
go back to reference 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) 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)
42.
go back to reference Papadopoulos, G.A., Arbab, F.: Coordination models and languages. Adv. Comput. 46, 329–400 (1998)CrossRef Papadopoulos, G.A., Arbab, F.: Coordination models and languages. Adv. Comput. 46, 329–400 (1998)CrossRef
43.
go back to reference Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRefMATH Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRefMATH
44.
go back to reference Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)MATH Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)MATH
45.
go back to reference Rosenmüller, M., Siegmund, N., Apel, S., Saake, G.: Flexible feature binding in software product lines. Autom. Softw. Eng. 18(2), 163–197 (2011)CrossRef Rosenmüller, M., Siegmund, N., Apel, S., Saake, G.: Flexible feature binding in software product lines. Autom. Softw. Eng. 18(2), 163–197 (2011)CrossRef
46.
go back to reference 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) 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)
47.
go back to reference 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) CrossRef 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) CrossRef
48.
go back to reference Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995) Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)
49.
go back to reference Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)MATHMathSciNet Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)MATHMathSciNet
50.
go back to reference 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)CrossRef 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)CrossRef
51.
go back to reference 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) 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)
52.
go back to reference 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) 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)
53.
go back to reference 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) 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)
54.
go back to reference 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) 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)
Metadata
Title
Probabilistic Model Checking for Feature-Oriented Systems
Authors
Clemens Dubslaff
Christel Baier
Sascha Klüppelholz
Copyright Year
2015
Publisher
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-46734-3_5

Premium Partner