{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:25:41Z","timestamp":1762521941181,"version":"3.41.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471655"},{"type":"electronic","value":"9783319471662"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47166-2_59","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T22:07:34Z","timestamp":1475618854000},"page":"856-873","source":"Crossref","is-referenced-by-count":18,"title":["Supervisory Controller Synthesis for Product Lines Using CIF\u00a03"],"prefix":"10.1007","author":[{"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel A.","family":"Reniers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erik P.","family":"de Vink","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"59_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-642-34026-0_12","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"P Asirelli","year":"2012","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A compositional framework to derive product line behavioural descriptions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 146\u2013161. Springer, Heidelberg (2012)"},{"key":"59_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"59_CR3","doi-asserted-by":"crossref","first-page":"811","DOI":"10.1007\/s10270-014-0441-1","volume":"15","author":"K Ba\u0327k","year":"2015","unstructured":"Ba\u0327k, K., Diskin, Z., Antkiewicz, M., Czarnecki, K., Wa\u0327sowski, A.: Clafer: unifying class and feature modeling. Softw. Syst. Model. 15, 811\u2013845 (2015)","journal-title":"Softw. Syst. Model."},{"key":"59_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-662-45234-9_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"MH Beek ter","year":"2014","unstructured":"ter Beek, M.H., de Vink, E.P.: Towards modular verification of software product lines with mCRL2. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 368\u2013385. Springer, Heidelberg (2014)"},{"key":"59_CR5","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink, E.P.: Using mCRL2 for the analysis of software product lines. In: FormaliSE 2014, pp. 31\u201337. IEEE (2014)","DOI":"10.1145\/2593489.2593493"},{"key":"59_CR6","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Towards a feature mu-Calculus targeting SPL verification. In: FMSPLE 2016, EPTCS, vol. 206, pp. 61\u201375 (2016)","DOI":"10.4204\/EPTCS.206.6"},{"issue":"2","key":"59_CR7","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/j.jlamp.2015.11.006","volume":"85","author":"MH Beek ter","year":"2016","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Methods Program. 85(2), 287\u2013315 (2016)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"59_CR8","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Legay, A., Lafuente, A.L., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: SPLC 2015, pp. 11\u201315. ACM (2015)","DOI":"10.1145\/2791060.2791087"},{"key":"59_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/978-3-319-47166-2_8","volume-title":"ISoLA 2016","author":"MH Beek ter","year":"2016","unstructured":"ter Beek, M.H., Legay, A., Lafuente, A.L., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114\u2013133. Springer, Heidelberg (2016)"},{"key":"59_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/978-3-642-32759-9_36","volume-title":"FM 2012: Formal Methods","author":"MH Beek ter","year":"2012","unstructured":"ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450\u2013454. Springer, Heidelberg (2012)"},{"key":"59_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1007\/978-3-642-54862-8_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DA Beek van","year":"2014","unstructured":"van Beek, D.A., Fokkink, W.J., Hendriks, D., Hofkamp, A., Markovski, J., van de Mortel-Fronczak, J.M., Reniers, M.A.: CIF 3: model-based engineering of supervisory controllers. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 575\u2013580. Springer, Heidelberg (2014)"},{"key":"59_CR12","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST 2006, pp. 125\u2013126. IEEE (2006)","DOI":"10.1109\/QEST.2006.59"},{"issue":"6","key":"59_CR13","doi-asserted-by":"crossref","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."},{"key":"59_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/978-3-662-45231-8_9","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"R Bubel","year":"2014","unstructured":"Bubel, R., H\u00e4hnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 120\u2013134. Springer, Heidelberg (2014)"},{"issue":"5","key":"59_CR15","doi-asserted-by":"crossref","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. Int. J. Softw. Tools Technol. Transfer 14(5), 589\u2013612 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"59_CR16","doi-asserted-by":"crossref","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":"59_CR17","doi-asserted-by":"crossref","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. Software Eng. 39(8), 1069\u20131089 (2013)","journal-title":"IEEE Trans. Software Eng."},{"key":"59_CR18","doi-asserted-by":"crossref","unstructured":"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: ICSE 2010, pp. 335\u2013344. ACM (2010)","DOI":"10.1145\/1806799.1806850"},{"key":"59_CR19","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: SPLC 2013, vol. 2, pp. 141\u2013146. ACM (2013)","DOI":"10.1145\/2499777.2499781"},{"key":"59_CR20","doi-asserted-by":"crossref","unstructured":"Delaware, B., Cook, W.R., Batory, D.S.: Product lines of theorems. In: Lopes, C.V., Fisher, K., (eds.) OOPSLA 2011, pp. 595\u2013608. ACM (2011)","DOI":"10.1145\/2048066.2048113"},{"issue":"3","key":"59_CR21","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/BF01933419","volume":"8","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: A constructive approach to the problem of program correctness. BIT Numer. Math. 8(3), 174\u2013186 (1968)","journal-title":"BIT Numer. Math."},{"issue":"4","key":"59_CR22","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1007\/s10626-012-0130-6","volume":"22","author":"STJ Forschelen","year":"2012","unstructured":"Forschelen, S.T.J., van de Mortel-Fronczak, J.M., Su, R., Rooda, J.E.: Application of supervisory control theory to theme park vehicles. Discrete Event Dyn. Syst. 22(4), 511\u2013540 (2012)","journal-title":"Discrete Event Dyn. Syst."},{"issue":"5","key":"59_CR23","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1109\/3477.875441","volume":"30","author":"P Gohari","year":"2000","unstructured":"Gohari, P., Wonham, W.M.: On the complexity of supervisory control design in the RW framework. IEEE Trans. Syst. Man Cybern. 30(5), 643\u2013652 (2000). Part\u00a0B","journal-title":"IEEE Trans. Syst. Man Cybern."},{"key":"59_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113\u2013131. Springer, Heidelberg (2008)"},{"key":"59_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/978-3-642-34026-0_4","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"R H\u00e4hnle","year":"2012","unstructured":"H\u00e4hnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 32\u201346. Springer, Heidelberg (2012)"},{"key":"59_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/3-540-45614-7_13","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"A Hall","year":"2002","unstructured":"Hall, A.: Correctness by construction: integrating formality into a commercial development process. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 224\u2013233. Springer, Heidelberg (2002)"},{"issue":"1","key":"59_CR27","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/52.976937","volume":"19","author":"A Hall","year":"2002","unstructured":"Hall, A., Chapman, R.: Correctness by construction: developing a commercial secure system. IEEE Softw. 19(1), 18\u201325 (2002)","journal-title":"IEEE Softw."},{"issue":"1","key":"59_CR28","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/362452.362489","volume":"14","author":"CAR Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Proof of a program: FIND. Commun. ACM 14(1), 39\u201345 (1971)","journal-title":"Commun. ACM"},{"key":"59_CR29","volume-title":"Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D., Abstractions, S.: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"59_CR30","unstructured":"Juodisius, P., Sarkar, A., Mukkamala, R.R., Antkiewicz, M., Czarnecki, K., Wa\u0327sowski, A.: Clafer: lightweight modeling of structure and behavior with variability. Unpublished manuscript"},{"key":"59_CR31","doi-asserted-by":"crossref","unstructured":"Lauenroth, K., Pohl, K., T\u00f6hning, S.: Model checking of domain artifacts in product line engineering. In: ASE 2009, pp. 269\u2013280. IEEE (2009)","DOI":"10.1109\/ASE.2009.16"},{"key":"59_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/978-3-642-34026-0_11","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"M Leucker","year":"2012","unstructured":"Leucker, M., Thoma, D.: A formal approach to software product families. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 131\u2013145. Springer, Heidelberg (2012)"},{"key":"59_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1007\/978-3-662-45234-9_23","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"M Lochau","year":"2014","unstructured":"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\u2013335. Springer, Heidelberg (2014)"},{"key":"59_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/978-3-540-24667-1_16","volume-title":"Software Product-Family Engineering","author":"M Mannion","year":"2004","unstructured":"Mannion, M., Camara, J.: Theorem proving for product line model verification. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 211\u2013224. Springer, Heidelberg (2004)"},{"key":"59_CR35","doi-asserted-by":"crossref","unstructured":"Markovski, J., Jacobs, K.G.M., van Beek, D.A., Somers, L.J.A.M., Rooda, J.E.: Coordination of resources using generalized state-based requirements. In: Raisch, J., Giua, A., Lafortune, S., Moor, T. (eds.) WODES 2010, pp. 287\u2013292. International Federation of Automatic Control (2010)","DOI":"10.3182\/20100830-3-DE-4013.00048"},{"issue":"3","key":"59_CR36","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1109\/TASE.2011.2124457","volume":"8","author":"L Ouedraogo","year":"2011","unstructured":"Ouedraogo, L., Kumar, R., Malik, R., \u00c5kesson, K.: Nonblocking and safe control of discrete-event systems modeled as extended finite automata. IEEE Trans. Autom. Sci. Eng. 8(3), 560\u2013569 (2011)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"59_CR37","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering: Foundations, Principles, and Techniques","author":"K Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, Heidelberg (2005)"},{"issue":"1","key":"59_CR38","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"PJ Ramadge","year":"1987","unstructured":"Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206\u2013230 (1987)","journal-title":"SIAM J. Control Optim."},{"volume-title":"Handbook of Automated Reasoning","year":"2001","key":"59_CR39","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. MIT Press, Cambridge (2001)"},{"key":"59_CR40","unstructured":"Schaefer, I.: Variability modelling for model-driven development of software product lines. In: Benavides, D., Batory, D.S., Gr\u00fcnbacher, P. (eds.) VaMoS 2010, ICB-Research report, vol. 37, pp. 85\u201392. Universit\u00e4t Duisburg-Essen (2010)"},{"key":"59_CR41","doi-asserted-by":"crossref","unstructured":"Skoldstam, M., \u00c5kesson, K., Fabian, M.: Modeling of discrete event systems using finite automata with variables. In: CDC 2007, pp. 3387\u20133392 (2007)","DOI":"10.1109\/CDC.2007.4434894"},{"key":"59_CR42","doi-asserted-by":"crossref","unstructured":"van der Sanden, B., Reniers, M.A., Geilen, M., Basten, T., Jacobs, J., Voeten, J., Schiffelers, R.R.H.: Modular model-based supervisory controller design for wafer logistics in lithography machines. In: MoDELS 2015, pp. 416\u2013425. IEEE (2015)","DOI":"10.1109\/MODELS.2015.7338273"},{"key":"59_CR43","doi-asserted-by":"crossref","unstructured":"Swartjes, L., Reniers, M.A., van Beek, D., Fokkink, W.: Why is my supervisor empty? Finding causes for the unreachability of states in synthesized supervisors. In: Cassandras, C.G., Giua, A., Li, Z. (eds.) WODES 2016, pp. 14\u201321. IEEE (2016)","DOI":"10.1109\/WODES.2016.7497820"},{"issue":"3","key":"59_CR44","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1016\/j.aei.2012.02.009","volume":"26","author":"RJM Theunissen","year":"2012","unstructured":"Theunissen, R.J.M., van Beek, D.A., Rooda, J.E.: Improving evolvability of a patient communication control system using state-based supervisory control synthesis. Adv. Eng. Inform. 26(3), 502\u2013515 (2012)","journal-title":"Adv. Eng. Inform."},{"key":"59_CR45","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: GPCE 2012, pp. 11\u201320. ACM (2012)","DOI":"10.1145\/2371401.2371404"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_59","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T23:11:41Z","timestamp":1749597101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_59"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_59","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}