{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:26:25Z","timestamp":1777519585522,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496640","type":"print"},{"value":"9783662496657","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49665-7_17","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T08:09:42Z","timestamp":1458547782000},"page":"287-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Family-Based Modeling and Analysis for Probabilistic Systems \u2013 Featuring ProFeat"],"prefix":"10.1007","author":[{"given":"Philipp","family":"Chrszon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clemens","family":"Dubslaff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5","key":"17_CR1","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/1745312.1745316","volume":"32","author":"S Apel","year":"2010","unstructured":"Apel, S., Hutchins, D.: A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. 32(5), 19:1\u201319:33 (2010)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-02408-5_2","volume-title":"Theory and Practice of Model Transformations","author":"S Apel","year":"2009","unstructured":"Apel, S., Janda, F., Trujillo, S., K\u00e4stner, C.: Model superimposition in software product lines. In: Paige, R.F. (ed.) ICMT 2009. LNCS, vol. 5563, pp. 4\u201319. Springer, Heidelberg (2009)"},{"issue":"5","key":"17_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.5381\/jot.2009.8.5.c5","volume":"8","author":"S Apel","year":"2009","unstructured":"Apel, S., K\u00e4stner, C.: An overview of feature-oriented software development. J. Object Technol. 8(5), 49\u201384 (2009)","journal-title":"J. Object Technol."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Apel, S., von Rhein, A., Wendler, P., Groesslinger, A., Beyer, D.: Strategies for product-line verification: Case studies and experiments. In: Proceedings of the International Conference on Software Engineering, ICSE 2013, pp. 482\u2013491. IEEE (2013)","DOI":"10.1109\/ICSE.2013.6606594"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Apel, S., Speidel, H., Wendler, P., von Rhein, A., Beyer, D.: Detection of feature interactions using feature-aware verification. In: International Conference on Automated Software Engineering (ASE), pp. 372\u2013375. IEEE (2011)","DOI":"10.1109\/ASE.2011.6100075"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-38088-4_21","volume-title":"NASA Formal Methods","author":"C Baier","year":"2013","unstructured":"Baier, C., Engel, B., Kl\u00fcppelholz, S., M\u00e4rcker, S., Tews, H., V\u00f6lp, M.: A probabilistic quantitative analysis of probabilistic-Write\/Copy-select. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 307\u2013321. Springer, Heidelberg (2013)"},{"issue":"6","key":"17_CR7","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1016\/j.is.2010.01.001","volume":"35","author":"D Benavides","year":"2010","unstructured":"Benavides, D., Segura, S., Ruiz-Cort\u00e9s, A.: Automated analysis of feature models 20 years later: A literature review. Inf. Syst. 35(6), 615\u2013636 (2010)","journal-title":"Inf. Syst."},{"issue":"12","key":"17_CR8","doi-asserted-by":"publisher","first-page":"1130","DOI":"10.1016\/j.scico.2010.10.005","volume":"76","author":"A Classen","year":"2011","unstructured":"Classen, A., Boucher, Q., Heymans, P.: A text-based approach to feature modelling: Syntax and semantics of TVL. Sci. Comput. Program. 76(12), 1130\u20131143 (2011)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"17_CR9","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-012-0234-1","volume":"14","author":"A Classen","year":"2012","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: Model checking software product lines with SNIP. STTT 14(5), 589\u2013612 (2012)","journal-title":"STTT"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1016\/j.scico.2013.09.019","volume":"80","author":"A Classen","year":"2014","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, 416\u2013439 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"8","key":"17_CR11","doi-asserted-by":"publisher","first-page":"1069","DOI":"10.1109\/TSE.2012.86","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen, A., Cordy, M., Schobbens, P.-Y., Heymans, P., Legay, A., Raskin, J.-F.: Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069\u20131089 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR12","volume-title":"Software Product Lines: Practices and Patterns","author":"P Clements","year":"2001","unstructured":"Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley Professional, Reading (2001)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-36249-1_1","volume-title":"Assurances for Self-Adaptive Systems","author":"M Cordy","year":"2013","unstructured":"Cordy, M., Classen, A., Heymans, P., Legay, A., Schobbens, P.-Y.: Model checking adaptive software with featured transition systems. In: C\u00e1mara, J., Lemos, R., Ghezzi, C., Lopes, A. (eds.) Assurances for Self-Adaptive Systems. LNCS, vol. 7740, pp. 1\u201329. Springer, Heidelberg (2013)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Cordy, M., Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: ProVeLines: a product line of verifiers for software product lines. In: 17th International Software Product Line Conference (SPLC), pp. 141\u2013146. ACM (2013)","DOI":"10.1145\/2499777.2499781"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"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 International Conference on Software Engineering, ICSE 2013, pp. 472\u2013481. IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606593"},{"issue":"1","key":"17_CR16","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1002\/spip.213","volume":"10","author":"K Czarnecki","year":"2005","unstructured":"Czarnecki, K., Helsen, S., Eisenecker, U.W.: Formalizing cardinality-based feature models and their specialization. Softw. Process: Improv. Pract. 10(1), 7\u201329 (2005)","journal-title":"Softw. Process: Improv. Pract."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Damiani, F., Schaefer, I.: Dynamic delta-oriented programming. In: Proceedings of the 15th International Software Product Line Conference, SPLC 2011. ACM (2011)","DOI":"10.1145\/2019136.2019175"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., \u00c1brah\u00e1m, E.: PROPhESY: A PRObabilistic parameter synthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Heidelberg (2015)"},{"key":"17_CR20","unstructured":"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)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/978-3-662-46734-3_5","volume-title":"Transactions on Aspect-Oriented Software Development XII","author":"C Dubslaff","year":"2015","unstructured":"Dubslaff, C., Baier, C., Kl\u00fcppelholz, S.: Probabilistic model checking for feature-oriented systems. In: Chiba, S., Tanter, \u00c9., Ernst, E., Hirschfeld, R. (eds.) Transactions on AOSD XII. LNCS, vol. 8989, pp. 180\u2013220. Springer, Heidelberg (2015)"},{"issue":"2","key":"17_CR22","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s00165-011-0207-2","volume":"24","author":"A Filieri","year":"2012","unstructured":"Filieri, A., Ghezzi, C., Tamburrelli, G.: A formal approach to adaptive software: Continuous assurance of non-functional requirements. Formal Aspects Comput. 24(2), 163\u2013186 (2012)","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"17_CR23","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1016\/j.infsof.2012.07.017","volume":"55","author":"C Ghezzi","year":"2013","unstructured":"Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Inf. Softw. Technol. 55(3), 508\u2013524 (2013)","journal-title":"Inf. Softw. Technol."},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-540-24667-1_33","volume-title":"Software Product-Family Engineering","author":"H Gomaa","year":"2004","unstructured":"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\u2013444. Springer, Heidelberg (2004)"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-68863-1_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"A Gruler","year":"2008","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113\u2013131. Springer, Heidelberg (2008)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: A model checker for parametric markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010)"},{"issue":"1","key":"17_CR27","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011)","journal-title":"Softw. Tools Technol. Transf."},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Palsberg, J., Hermanns, H. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"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 (1990)","DOI":"10.21236\/ADA235785"},{"issue":"2","key":"17_CR30","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1145\/169701.169682","volume":"15","author":"S Katz","year":"1993","unstructured":"Katz, S.: A superimposition control construct for distributed systems. ACM Trans. Program. Lang. Syst. 15(2), 337\u2013356 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Kl\u00fcppelholz, S., M\u00e4rcker, S., M\u00fcller, D.: Advances in symbolic probabilistic model checking with PRISM. In: Proceedings of the 22th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS. Springer, to appear (2016)","DOI":"10.1007\/978-3-662-49674-9_20"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-642-54804-8_7","volume-title":"Fundamental Approaches to Software Engineering","author":"M Kowal","year":"2014","unstructured":"Kowal, M., Schaefer, I., Tribastone, M.: Family-based performance analysis of variant-rich software systems. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 94\u2013108. Springer, Heidelberg (2014)"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of the Quantitative Evaluation of Systems (QEST 2012), pp. 203\u2013204. IEEE, 2012. \n                      https:\/\/github.com\/prismmodelchecker\/prism-benchmarks\/","DOI":"10.1109\/QEST.2012.14"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Lauenroth, K., Pohl, K., Toehning, S.: Model checking of domain artifacts in product line engineering. In: 24th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 269\u2013280. IEEE (2009)","DOI":"10.1109\/ASE.2009.16"},{"key":"17_CR35","doi-asserted-by":"crossref","unstructured":"Meinicke, J., Th\u00fcm, T., Schr\u00f6ter, R., Benduhn, F., Saake, G.: An overview on analysis tools for software product lines. In: 18th International Software Product Lines Conference (SPLC), pp. 94\u2013101. ACM (2014)","DOI":"10.1145\/2647908.2655972"},{"issue":"1","key":"17_CR36","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0167-6423(00)00018-6","volume":"41","author":"M Plath","year":"2001","unstructured":"Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53\u201384 (2001)","journal-title":"Sci. Comput. Program."},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Rodrigues, G.N., Alves, V., Nunes, V., Lanna, A., Cordy, M., Schobbens, P.-Y., Sharifloo, A.M., Legay, A.: Modeling and verification for probabilistic properties in software product lines. In: High Assurance Systems Engineering (HASE), pp. 173\u2013180. IEEE (2015)","DOI":"10.1109\/HASE.2015.34"},{"key":"17_CR38","unstructured":"Segura, S.: Automated analysis of feature models using atomic sets. In: SPLC (2), pp. 201\u2013207 (2008)"},{"key":"17_CR39","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Legay, A., Lluch-Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: 19th International Conference on Software Product Line (SPLC), pp. 11\u201315. ACM (2015)","DOI":"10.1145\/2791060.2791087"},{"key":"17_CR40","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.scico.2012.06.002","volume":"79","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm, T., K\u00e4stner, C., Benduhn, F., Meinicke, J., Saake, G., Leich, T.: FeatureIDE: An extensible framework for feature-oriented software development. Sci. Comput. Program. 79, 70\u201385 (2014)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49665-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:11:36Z","timestamp":1585012296000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}