{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T14:13:54Z","timestamp":1742998434383,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319301419"},{"type":"electronic","value":"9783319301426"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30142-6_17","type":"book-chapter","created":{"date-parts":[[2016,2,24]],"date-time":"2016-02-24T11:36:41Z","timestamp":1456313801000},"page":"307-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Feature Interactions"],"prefix":"10.1007","author":[{"given":"Thibaut","family":"Le Guilly","sequence":"first","affiliation":[]},{"given":"Petur","family":"Olsen","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Pedersen","sequence":"additional","affiliation":[]},{"given":"Anders P.","family":"Ravn","sequence":"additional","affiliation":[]},{"given":"Arne","family":"Skou","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,25]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/2.223539","volume":"26","author":"P Zave","year":"1993","unstructured":"Zave, P.: Feature interactions and formal specifications in telecommunications. Computer 26, 20\u201328 (1993)","journal-title":"Computer"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1109\/32.729680","volume":"24","author":"D Keck","year":"1998","unstructured":"Keck, D., Kuehn, P.: The feature and service interaction problem in telecommunications systems: a survey. IEEE Trans. Softw. Eng. 24, 779\u2013796 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/s11219-011-9165-4","volume":"20","author":"M Lochau","year":"2012","unstructured":"Lochau, M., Oster, S., Goltz, U., Sch\u00fcrr, A.: Model-based pairwise testing for feature interaction coverage in software product line engineering. Softw. Qual. J. 20, 567\u2013604 (2012)","journal-title":"Softw. Qual. J."},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"2429","DOI":"10.1016\/j.comnet.2013.02.026","volume":"57","author":"C Maternaghan","year":"2013","unstructured":"Maternaghan, C., Turner, K.J.: Policy conflicts in home automation. Comput. Netw. 57, 2429\u20132441 (2013)","journal-title":"Comput. Netw."},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"1428","DOI":"10.3844\/jcssp.2014.1428.1439","volume":"10","author":"IA Al-Baltah","year":"2014","unstructured":"Al-Baltah, I.A., Ghani, A.A.A., Ab Rahman, W.N.W., Atan, R.: Semantic conflicts detection of heterogeneous messages of web services: challenges and solution. J. Comput. Sci. 10, 1428 (2014)","journal-title":"J. Comput. Sci."},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/S1389-1286(02)00352-3","volume":"41","author":"M Calder","year":"2003","unstructured":"Calder, M., Kolberg, M., Magill, E.H., Reiff-Marganiec, S.: Feature interaction: a critical review and considered forecast. Comput. Netw. 41, 115\u2013141 (2003)","journal-title":"Comput. Netw."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Pedersen, T., Le Guilly, T., Ravn, A., Skou, A.: A method for model checking feature interactions. In: Proceedings of the 10th International Conference on Software Engineering and Applications, pp. 219\u2013228 (2015)","DOI":"10.5220\/0005516402190228"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"R\u00e9p\u00e1si, T., Giessl, S., Prehofer, C.: Using model-checking for the detection of non-functional feature interactions. In: 2012 IEEE 16th International Conference on Intelligent Engineering Systems (INES), pp. 167\u2013172. IEEE (2012)","DOI":"10.1109\/INES.2012.6249825"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1109\/MCOM.2003.1244934","volume":"41","author":"M Kolberg","year":"2003","unstructured":"Kolberg, M., Magill, E.H., Wilson, M.: Compatibility issues between services supporting networked appliances. IEEE Commun. Mag. 41, 136\u2013147 (2003)","journal-title":"IEEE Commun. Mag."},{"key":"17_CR11","unstructured":"Wilson, M., Kolberg, M., Magill, E.H.: Considering side effects in service interactions in home automation-an online approach. In: Feature Interactions in Software and Communication Systems IX, p. 172 (2008)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Le Guilly, T., Olsen, P., Ravn, A.P., Skou, A.: Modelling and analysis of component faults and reliability. In: Petre, L., Sekerinski, E. (eds.) From Action System to Distributed Systems: The Refinement Approach (2015, accepted for publication)","DOI":"10.1201\/b20053-7"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-78743-3_2","volume-title":"Fundamental Approaches to Software Engineering","author":"A Classen","year":"2008","unstructured":"Classen, A., Heymans, P., Schobbens, P.-Y.: What\u2019s in a feature: a requirements engineering perspective. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 16\u201330. Springer, Heidelberg (2008)"},{"key":"17_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07287-5","volume-title":"Formal Engineering for Industrial Software Development","author":"S Liu","year":"2004","unstructured":"Liu, S.: Formal Engineering for Industrial Software Development. Springer, Heidelberg (2004)"},{"key":"17_CR15","unstructured":"Behrmann, G., David, R., Larsen, K.G.: A tutorial on Uppaal 4.0 (2006)"},{"key":"17_CR16","unstructured":"Wilson, M., Magill, E.H., Kolberg, M.: An online approach for the service interaction problem in home automation. In: Consumer Communications and Networking Conference, CCNC. 2005 Second IEEE, pp. 251\u2013256. IEEE (2005)"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-013-0275-0","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17, 1\u201319 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR18","unstructured":"Nakamura, M., Igaki, H., Matsumoto, K.I.: Feature interactions in integrated services of networked home appliances. In: Proceedings of International Conference on Feature Interactions in Telecommunication Networks and Distributed Systems (ICFI05), pp. 236\u2013251 (2005)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Leelaprute, P., Nakamura, M., Tsuchiya, T., Matsumoto, K.I., Kikuno, T. : Describing and verifying integrated services of home network systems. In: Software Engineering Conference, APSEC 2005. 12th Asia-Pacific, p. 10 (2005)","DOI":"10.1109\/APSEC.2005.59"},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: a new symbolic model checker. Int. J. Softw. Tools Technol. Transfer 2, 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"17_CR21","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s11334-009-0092-5","volume":"5","author":"L Bousquet du","year":"2009","unstructured":"du Bousquet, L., Nakamura, M., Yan, B., Igaki, H.: Using formal methods to increase confidence in a home network system implementation: a case study. Innovations Syst. Softw. Eng. 5, 181\u2013196 (2009)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"8447","DOI":"10.3390\/s120708447","volume":"12","author":"T Inada","year":"2012","unstructured":"Inada, T., Igaki, H., Ikegami, K., Matsumoto, S., Nakamura, M., Kusumoto, S.: Detecting service chains and feature interactions in sensor-driven home network services. Sensors 12, 8447\u20138464 (2012)","journal-title":"Sensors"},{"key":"17_CR23","doi-asserted-by":"publisher","first-page":"2442","DOI":"10.1016\/j.comnet.2013.02.024","volume":"57","author":"M Nakamura","year":"2013","unstructured":"Nakamura, M., Ikegami, K., Matsumoto, S.: Considering impacts and requirements for better understanding of environment interactions in home network services. Comput. Netw. 57, 2442\u20132453 (2013)","journal-title":"Comput. Netw."},{"key":"17_CR24","unstructured":"Metzger, A., Webel, C.: Feature interaction detection in building control systems by means of a formal product model. In: FIW, pp. 105\u2013122 (2003)"},{"key":"17_CR25","doi-asserted-by":"crossref","first-page":"1582","DOI":"10.1002\/sec.794","volume":"7","author":"F Corno","year":"2014","unstructured":"Corno, F., Sanaullah, M.: Modeling and formal verification of smart environments. Secur. Commun. Netw. 7, 1582\u20131598 (2014)","journal-title":"Secur. Commun. Netw."},{"key":"17_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2298\/CSIS0701001A","volume":"4","author":"JC Augusto","year":"2007","unstructured":"Augusto, J.C., McCullagh, P.: Ambient intelligence: concepts and applications. Comput. Sci. Inf. Syst. 4, 1\u201327 (2007)","journal-title":"Comput. Sci. Inf. Syst."},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-38088-4_24","volume-title":"NASA Formal Methods","author":"A David","year":"2013","unstructured":"David, A., Du, D., Guldstrand Larsen, K., Legay, A., Miku\u010dionis, M.: Optimizing control strategy using statistical model checking. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 352\u2013367. Springer, Heidelberg (2013)"},{"key":"17_CR28","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: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering, vol. 1, pp. 335\u2013344. ACM (2010)","DOI":"10.1145\/1806799.1806850"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I\/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 91\u2013100. ACM (2010)","DOI":"10.1145\/1755952.1755967"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-73035-4_14","volume-title":"Pervasive Computing for Quality of Life Enhancement","author":"B Yan","year":"2007","unstructured":"Yan, B., Nakamura, M., du Bousquet, L., Matsumoto, K.: Characterizing safety of integrated services in home network system. In: Okadome, T., Yamazaki, T., Makhtari, M. (eds.) ICOST. LNCS, vol. 4541, pp. 130\u2013140. Springer, Heidelberg (2007)"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-540-75454-1_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"JJ Jessen","year":"2007","unstructured":"Jessen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using Uppaal Tiga. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 227\u2013240. Springer, Heidelberg (2007)"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121\u2013125. Springer, Heidelberg (2007)"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Dalsgaard, P.H., Le Guilly, T., Middelhede, D., Olsen, P., Pedersen, T., Ravn, A.P., Skou, A.: A toolchain for home automation controller development. In: 2013 39th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pp. 122\u2013129. IEEE (2013)","DOI":"10.1109\/SEAA.2013.36"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Le Guilly, T., Smedegard, J.H., Pedersen, T., Skou, A.: To do and not to do: constrained scenarios for safe smart house. In: 2015 International Conference on Intelligent Environments (IE), pp. 17\u201324 (2015)","DOI":"10.1109\/IE.2015.11"}],"container-title":["Communications in Computer and Information Science","Software Technologies"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30142-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,16]],"date-time":"2020-09-16T01:16:53Z","timestamp":1600219013000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30142-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319301419","9783319301426"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30142-6_17","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"25 February 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}