Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Statistical Model Checking: Past, Present, and Future Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Statistical Model Checking for Product Lines

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

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

Publisher: Springer International Publishing

Log in

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

search-config
loading …

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.

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!

inform now

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!

inform now

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!

inform now
previous chapter Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego
next chapter Towards Adaptive Scheduling of Maintenance for Cyber-Physical Systems
Footnotes
1
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 \).
 
Literature
1.
Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. ENTCS 153, 213–239 (2005)
2.
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
3.
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)
4.
Baier, C., Katoen, J.: Principles of Model Checking. The MIT Press, Cambridge (2008)MATH
5.
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
6.
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
7.
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
8.
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
9.
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.
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.
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.
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)
Metadata
Title
Statistical Model Checking for Product Lines
Authors
Maurice H. ter Beek
Axel Legay
Alberto Lluch Lafuente
Andrea Vandin
Copyright Year
2016
Book
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 Year: 2016

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

Premium Partner

    Image Credits