nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Statistical Model Checking for Product Lines

verfasst von : Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin

Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We report on the suitability of statistical model checking for the analysis of quantitative properties of product line models by an extended treatment of earlier work by the authors. The type of analysis that can be performed includes the likelihood of specific product behaviour, the expected average cost of products (in terms of the attributes of the products’ features) and the probability of features to be (un)installed at runtime. The product lines must be modelled in QFLan, which extends the probabilistic feature-oriented language PFLan with novel quantitative constraints among features and on behaviour and with advanced feature installation options. QFLan is a rich process-algebraic specification language whose operational behaviour interacts with a store of constraints, neatly separating product configuration from product behaviour. The resulting probabilistic configurations and probabilistic behaviour converge in a discrete-time Markov chain semantics, enabling the analysis of quantitative properties. Technically, a Maude implementation of QFLan, integrated with Microsoft’s SMT constraint solver Z3, is combined with the distributed statistical model checker MultiVeStA, developed by one of the authors. We illustrate the feasibility of our framework by applying it to a case study of a product line of bikes.

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 Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego

Nächstes Kapitel Towards Adaptive Scheduling of Maintenance for Cyber-Physical Systems

The attribute functions extend to non-primitive features and products in a straightforward manner (e.g. the function \(\textit{load} :\mathcal{F} \rightarrow \mathbb {N}\), associated to the attribute load, extends to \(\textit{load}\,(\mathcal{P}_\mathcal{F}) = \textstyle {\sum }\,\lbrace \,\textit{load}\,(f)\mid f\in \mathcal{P}_\mathcal{F}\,\rbrace \).

Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. ENTCS 153, 213–239 (2005)

AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22944-2_28 CrossRef

Arora, S., Rathor, A., Rao, M.V.P.: Statistical model checking of opportunistic network protocols. In: Proceedings 11th Asian Internet Engineering Conference (AINTEC 2015), pp. 62–68. ACM (2015)

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

Bartoletti, M., Cimoli, T., Murgia, M., Podda, A.S., Pompianu, L.: A contract-oriented middleware. In: Braga, C., Ölveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 86–104. Springer, Heidelberg (2016). doi:10.1007/978-3-319-28934-2_5 CrossRef

Batory, D.: Feature models, grammars, and propositional formulas. In: Obbink, H., Pohl, K. (eds.) SPLC 2005. LNCS, vol. 3714, pp. 7–20. Springer, Heidelberg (2005). doi:10.1007/11554844_3 CrossRef

ter Beek, M.H., Clarke, D., Schaefer, I.: Special issue on formal methods in software product line engineering. J. Log. Algebr. Meth. Program. 85(1), 123–124 (2016)CrossRefMATH

ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Quantitative analysis of probabilistic models of software product lines with statistical model checking. EPTCS 182, 56–70 (2015)CrossRef

ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: Proceedings 19th International Software Product Line Conference (SPLC 2015), pp. 11–15. ACM (2015)

10.

ter Beek, M.H., Lluch Lafuente, A., Petrocchi, M.: Combining declarative and procedural views in the specification and analysis of product families. In: Proceedings 17th International Software Product Line Conference (SPLC 2013), vol. 2, pp. 10–17. ACM (2013)

11.

Belzner, L., De Nicola, R., Vandin, A., Wirsing, M.: Reasoning (on) service component ensembles in rewriting logic. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 188–211. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54624-2_10 CrossRef

12.

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

13.

Borba, P., Cohen, M.B., Legay, A., Wąsowski, A.: Analysis, test and verification in the presence of variability. Dagstuhl Rep. 3(2), 144–170 (2013)

14.

Bortolussi, L.: Stochastic concurrent constraint programming. ENTCS 164, 65–80 (2006)

15.

Buscemi, M.G., Montanari, U.: CC-Pi: a constraint-based language for specifying service level agreements. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 18–32. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71316-6_3 CrossRef

16.

Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: Family-based modeling and analysis for probabilistic systems – featuring ProFeat. In: Stevens, P., Wasowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 287–304. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49665-7_17 CrossRef

17.

Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013)CrossRef

18.

Clavel, M. (ed.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71999-1

19.

Cordy, M., Schobbens, P., Heymans, P., Legay, A.: Beyond Boolean product-line model checking: dealing with feature attributes and multi-features. In: Proceedings 35th International Conference on Software Engineering (ICSE 2013), pp. 472–481. IEEE (2013)

20.

de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24 CrossRef

21.

Dubslaff, C., Baier, C., Klüppelholz, S.: Probabilistic model checking for feature-oriented systems. In: Chiba, S., Tanter, É., Ernst, E., Hirschfeld, R. (eds.) Transactions on AOSD XII. LNCS, vol. 8989, pp. 180–220. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46734-3_5

22.

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

23.

Erwig, M., Walkingshaw, E.: The choice calculus: a representation for software variation. ACM Trans. Softw. Eng. Methodol. 21(1), 6 (2011)CrossRef

24.

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

25.

Gilmore, S., Tribastone, M., Vandin, A.: An analysis pathway for the quantitative evaluation of public transport systems. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 71–86. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10181-1_5

26.

Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8802, pp. 135–142. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8_10

27.

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). doi:10.1007/978-3-642-16612-9_11 CrossRef

28.

Lochau, M., Mennicke, S., Baller, H., Ribbeck, L.: DeltaCCS: a core calculus for behavioral change. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 320–335. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45234-9_23

29.

Rodrigues, G.N., et al.: Modeling and verification for probabilistic properties in software product lines. In: Proceedings 16th International Symposium on High Assurance Systems Engineering (HASE 2015), pp. 173–180. IEEE (2015)

30.

Pianini, D., Sebastio, S., Vandin, A.: Distributed statistical analysis of complex systems modeled through a chemical metaphor. In: Proceedings International Conference on High Performance Computing and Simulation (HPCS 2014), pp. 416–423. IEEE (2014)

31.

Saraswat, V., Rinard, M.: Concurrent constraint programming. In: Conference Record 17th Annual Symposium on Principles of Programming Languages (POPL 1990), pp. 232–245. ACM (1990)

32.

Schaefer, I., Hähnle, R.: Formal methods in software product line engineering. IEEE Comput. 44(2), 82–85 (2011)CrossRef

33.

Sebastio, S., Amoretti, M., Lluch Lafuente, A.: A computational field framework for collaborative task execution in volunteer clouds. In: Proceedings 9th International Symposium on Software Engineering for Adaptive and Self-managing Systems (SEAMS 2014), pp. 105–114. ACM (2014)

34.

Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Proceedings 7th International Conference on Performance Evaluation Methodologies and Tools (ValueTools 2013), pp. 310–315. ACM (2013)

35.

Sen, K., Viswanathan, M., Agha, G.A., VESTA: a statistical model-checker and analyzer for probabilistic systems. In: Proceedings 2nd International Conference on Quantitative Evaluation of Systems (QEST 2005), pp. 251–252. IEEE (2005)

36.

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

37.

Tribastone, M.: Behavioral relations in a process algebra for variants. In: Proceedings 18th International Software Product Line Conference (SPLC 2014), pp. 82–91. ACM (2014)

38.

Varshosaz, M., Khosravi, R.: Families, discrete time Markov chain: modeling and verification of probabilistic software product lines. In: Proceedings 17th International Software Product Line Conference (SPLC 2013), vol. 2, pp. 34–41. ACM (2013)

Titel: Statistical Model Checking for Product Lines
verfasst von: Maurice H. ter Beek
Axel Legay
Alberto Lluch Lafuente
Andrea Vandin
Verlag: Springer International Publishing
Buch: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques
Print ISBN: 978-3-319-47165-5

Electronic ISBN: 978-3-319-47166-2

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-47166-2_8

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