{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:26:19Z","timestamp":1770297979517,"version":"3.49.0"},"reference-count":81,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,4,23]],"date-time":"2021-04-23T00:00:00Z","timestamp":1619136000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003593","name":"CNPq","doi-asserted-by":"crossref","award":["310757\/2018-5"],"award-info":[{"award-number":["310757\/2018-5"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003593","name":"CNPq","doi-asserted-by":"crossref","award":["465614\/2014-0"],"award-info":[{"award-number":["465614\/2014-0"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003593","name":"CNPq","doi-asserted-by":"crossref","award":["426005\/2018-0 and 311442\/2019-6"],"award-info":[{"award-number":["426005\/2018-0 and 311442\/2019-6"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003593","name":"CNPq","doi-asserted-by":"crossref","award":["409335\/2016-9"],"award-info":[{"award-number":["409335\/2016-9"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100002322","name":"CAPES","doi-asserted-by":"crossref","award":["117875 and 175956"],"award-info":[{"award-number":["117875 and 175956"]}],"id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["AP 206\/6 and AP 206\/11"],"award-info":[{"award-number":["AP 206\/6 and AP 206\/11"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"FNR Luxembourg","award":["C19\/IS\/13566661\/BEEHIVE\/Cordy"],"award-info":[{"award-number":["C19\/IS\/13566661\/BEEHIVE\/Cordy"]}]},{"DOI":"10.13039\/501100005668","name":"FAPDF","doi-asserted-by":"crossref","award":["00193-00000926\/2019-67"],"award-info":[{"award-number":["00193-00000926\/2019-67"]}],"id":[{"id":"10.13039\/501100005668","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100006162","name":"FACEPE","doi-asserted-by":"crossref","award":["APQ-0570-1.03\/14"],"award-info":[{"award-number":["APQ-0570-1.03\/14"]}],"id":[{"id":"10.13039\/501100006162","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100006162","name":"FACEPE","doi-asserted-by":"crossref","award":["APQ-0388-1.03\/14 and APQ-0399-1.03\/17"],"award-info":[{"award-number":["APQ-0388-1.03\/14 and APQ-0399-1.03\/17"]}],"id":[{"id":"10.13039\/501100006162","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2021,7,31]]},"abstract":"<jats:p>A number of product-line analysis approaches lift analyses such as type checking, model checking, and theorem proving from the level of single programs to the level of product lines. These approaches share concepts and mechanisms that suggest an unexplored potential for reuse of key analysis steps and properties, implementation, and verification efforts. Despite the availability of taxonomies synthesizing such approaches, there still remains the underlying problem of not being able to describe product-line analyses and their properties precisely and uniformly. We propose a formal framework that models product-line analyses in a compositional manner, providing an overall understanding of the space of family-based, feature-based, and product-based analysis strategies. It defines precisely how the different types of product-line analyses compose and inter-relate. To ensure soundness, we formalize the framework, providing mechanized specification and proofs of key concepts and properties of the individual analyses. The formalization provides unambiguous definitions of domain terminology and assumptions as well as solid evidence of key properties based on rigorous formal proofs. To qualitatively assess the generality of the framework, we discuss to what extent it describes five representative product-line analyses targeting the following properties: safety, performance, dataflow facts, security, and functional program properties.<\/jats:p>","DOI":"10.1145\/3442389","type":"journal-article","created":{"date-parts":[[2021,4,23]],"date-time":"2021-04-23T10:32:50Z","timestamp":1619173970000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A Formal Framework of Software Product Line Analyses"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5758-2097","authenticated-orcid":false,"given":"Thiago","family":"Castro","sequence":"first","affiliation":[{"name":"Systems Development Center\u2014Brazilian Army"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leopoldo","family":"Teixeira","sequence":"additional","affiliation":[{"name":"Federal University of Pernambuco"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vander","family":"Alves","sequence":"additional","affiliation":[{"name":"University of Bras\u00edlia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sven","family":"Apel","sequence":"additional","affiliation":[{"name":"Saarland University, Saarland Informatics Campus"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8312-1358","authenticated-orcid":false,"given":"Maxime","family":"Cordy","sequence":"additional","affiliation":[{"name":"University of Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rohit","family":"Gheyi","sequence":"additional","affiliation":[{"name":"Federal University of Campina Grande"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,4,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.120"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606594"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPLC.2011.34"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008699807402"},{"key":"e_1_2_1_6_1","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00038-6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2010.01.001"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491976"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.01.031"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36964-3_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.013"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380927"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628155"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1980.234477"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_17"},{"key":"e_1_2_1_18_1","volume-title":"Logic of Programs (LNCS)","volume":"131","author":"Clarke E. M.","unstructured":"E. M. Clarke and E. A. Emerson. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs (LNCS), Vol. 131. Springer, 52--71."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2748144.2748397"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.86"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806850"},{"key":"e_1_2_1_22_1","volume-title":"Software Product Lines: Practices and Patterns","author":"Clements Paul","unstructured":"Paul Clements and Linda Northrop. 2001. Software Product Lines: Practices and Patterns. Addison-Wesley Professional."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2110147.2110168"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30985-5_18"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635919"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606593"},{"key":"e_1_2_1_27_1","volume-title":"Eisenecker","author":"Czarnecki Krzysztof","year":"2000","unstructured":"Krzysztof Czarnecki and Ulrich W. Eisenecker. 2000. Generative Programming: Methods, Tools, and Applications. ACM Press\/Addison-Wesley Publishing Co., USA."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173738"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595733"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011","author":"Delaware Benjamin","year":"2011","unstructured":"Benjamin Delaware, William R. Cook, and Don S. Batory. 2011. Product lines of theorems. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22-27, 2011. ACM, 595--608. DOI:https:\/\/doi.org\/10.1145\/2048066.2048113"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00479-y"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-015-0503-z"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPLC.2008.45"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147249.1147254"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the IEEE 22nd International Symposium on Software Reliability Engineering. IEEE, 90--99","author":"Garvin B. J.","year":"2011","unstructured":"B. J. Garvin and M. B. Cohen. 2011. Feature interaction faults revisited: An exploratory study. In Proceedings of the IEEE 22nd International Symposium on Software Reliability Engineering. IEEE, 90--99. DOI:https:\/\/doi.org\/10.1109\/ISSRE.2011.25"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2012.07.017"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491445"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 7th Tagungsband - Dagstuhl-Workshop: Modellbasierte Entwicklung eingebetteter Systeme (MBEES). 1--10","author":"Haber Arne","year":"2011","unstructured":"Arne Haber, Holger Rendel, Bernhard Rumpe, and Ina Schaefer. 2011. Delta modeling for software architectures. In Proceedings of the 7th Tagungsband - Dagstuhl-Workshop: Modellbasierte Entwicklung eingebetteter Systeme (MBEES). 1--10."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0146-x"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34026-0_4"},{"key":"e_1_2_1_41_1","volume-title":"Spin Model Checker, the: Primer and Reference Manual","author":"Holzmann Gerard","unstructured":"Gerard Holzmann. 2003. Spin Model Checker, the: Primer and Reference Manual (first ed.). Addison-Wesley Professional."},{"key":"e_1_2_1_42_1","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"Huth Michael","unstructured":"Michael Huth, Radha Jagadeesan, and David Schmidt. 2001. Modal transition systems: A foundation for three-valued program analysis. In Programming Languages and Systems. Lecture Notes in Computer Science, Vol. 2028. Springer, 155--169."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"K. C. Kang S. G. Cohen J. A. Hess W. E. Novak and A. S. Peterson. 1990. Feature-Oriented Domain Analysis (FODA) Feasibility Study. Technical Report. Carnegie-Mellon University Software Engineering Institute.","DOI":"10.21236\/ADA235785"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368131"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1621607.1621632"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517208.2517213"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.16"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV) (Lecture Notes in Computer Science)","volume":"6806","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV) (Lecture Notes in Computer Science), Vol. 6806. Springer, 585--591. DOI:https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2017.10.001"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2018.05.007"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884793"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2647908.2655972"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.04.005"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238201"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2047862.2047869"},{"key":"e_1_2_1_58_1","volume-title":"PVS Language Reference. Computer Science Laboratory","author":"Owre S.","unstructured":"S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. 2001. PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-015-9364-x"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278122.3278126"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00018-6"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_63_1","volume-title":"van der Linden","author":"Pohl Klaus","year":"2005","unstructured":"Klaus Pohl, G\u00fcnter B\u00f6ckle, and Frank J. van der Linden. 2005. Software Product Line Engineering: Foundations, Principles and Techniques. Springer."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053389"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2015.34"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2019.04.051"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2006.08.008"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297064"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2791060.2791105"},{"key":"e_1_2_1_70_1","first-page":"22969","volume-title":"Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM). Springer, 344--359","author":"Beek Maurice H.","year":"2015","unstructured":"Maurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti, and Luca Paolini. 2015. From featured transition systems to modal transition systems with variability constraints. In Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM). Springer, 344--359. DOI:https:\/\/doi.org\/10.1007\/978-3-319-22969-0"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2018.09.006"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.11.006"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2580950"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2011.48"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307630.3342414"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/WICSA.2001.948406"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.03.003"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430502.2430522"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280986"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.06.007"},{"key":"e_1_2_1_81_1","volume-title":"Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, part of SPLASH \u201914","author":"Walkingshaw Eric","year":"2014","unstructured":"Eric Walkingshaw, Christian K\u00e4stner, Martin Erwig, Sven Apel, and Eric Bodden. 2014. Variational data structures: Exploring tradeoffs in computing with variability. In Onward! 2014, Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, part of SPLASH \u201914. ACM, 213--226. DOI:https:\/\/doi.org\/10.1145\/2661136.2661143"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.111.7"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3442389","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3442389","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:28Z","timestamp":1750195468000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3442389"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,23]]},"references-count":81,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,31]]}},"alternative-id":["10.1145\/3442389"],"URL":"https:\/\/doi.org\/10.1145\/3442389","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4,23]]},"assertion":[{"value":"2020-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}