nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Probabilistic Model Checking for Feature-Oriented Systems

verfasst von : Clemens Dubslaff, Christel Baier, Sascha Klüppelholz

Erschienen in: Transactions on Aspect-Oriented Software Development XII

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Reusable Components of Semantic Specifications

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.

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

Apel, S., Hutchins, D.: A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. 32(5), 1–33 (2010)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

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., 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., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)MATH

Baier, C., Kwiatkoswka, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125–155 (1998)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

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

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

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)

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

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)

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)

14.

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

15.

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

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

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)

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

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)

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

21.

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

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)

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)

24.

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

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

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

27.

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

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

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

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)

31.

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

32.

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

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)

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

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

36.

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

37.

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

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)

39.

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

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

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)

42.

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

43.

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

44.

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

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

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)

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

48.

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

49.

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

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

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)

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)

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)

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)

Titel: Probabilistic Model Checking for Feature-Oriented Systems
verfasst von: Clemens Dubslaff
Christel Baier
Sascha Klüppelholz
Verlag: Springer Berlin Heidelberg
Buch: Transactions on Aspect-Oriented Software Development XII
Print ISBN: 978-3-662-46733-6

Electronic ISBN: 978-3-662-46734-3

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-662-46734-3_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner