{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,15]],"date-time":"2025-07-15T03:35:02Z","timestamp":1752550502349},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,5,4]],"date-time":"2016-05-04T00:00:00Z","timestamp":1462320000000},"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":["J Reliable Intell Environ"],"published-print":{"date-parts":[[2016,7]]},"DOI":"10.1007\/s40860-016-0020-z","type":"journal-article","created":{"date-parts":[[2016,5,4]],"date-time":"2016-05-04T13:20:22Z","timestamp":1462368022000},"page":"75-91","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["User constraints for reliable user-defined smart home scenarios"],"prefix":"10.1007","volume":"2","author":[{"given":"Thibaut","family":"Le Guilly","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael K.","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Pedersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arne","family":"Skou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jesper","family":"Kjeldskov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikael","family":"Skov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,4]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive systems: modelling, specification and verification","author":"L Aceto","year":"2007","unstructured":"Aceto L, Ing\u00f3lfsd\u00f3ttir A, Larsen KG, Srba J (2007) Reactive systems: modelling, specification and verification. Cambridge University Press, New York"},{"key":"20_CR2","volume-title":"Notes on the synthesis of form","author":"C Alexander","year":"1964","unstructured":"Alexander C (1964) Notes on the synthesis of form. Harvard University Press, Harvard"},{"issue":"2","key":"20_CR3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"issue":"1","key":"20_CR4","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur R, Feder T, Henzinger TA (1996) The benefits of relaxing punctuality. J ACM 43(1):116\u2013146","journal-title":"J ACM"},{"key":"20_CR5","unstructured":"Augusto JC (2009) Increasing reliability in the development of intelligent environments. In: Proceedings of the 5th international conference on intelligent environments, IOS Press, pp 134\u2013141"},{"key":"20_CR6","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1016\/j.advengsoft.2012.12.004","volume":"58","author":"JC Augusto","year":"2013","unstructured":"Augusto JC, Hornos MJ (2013) Software simulation and verification to increase the reliability of intelligent environments. Adv Eng Softw 58:18\u201334","journal-title":"Adv Eng Softw"},{"key":"20_CR7","unstructured":"Augusto JC, Nugent CD (2004) The use of temporal reasoning and management of complex events in smart homes. In: ECAI, Citeseer, vol 16, p 778"},{"key":"20_CR8","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal methods for the design of real-time systems, lecture notes in computer science","author":"G Behrmann","year":"2004","unstructured":"Behrmann G, David A, Larsen K (2004) A tutorial on Uppaal. In: Bernardo M, Corradini F (eds) Formal methods for the design of real-time systems, lecture notes in computer science, vol 3185. Springer, Berlin, pp 200\u2013236"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Belarbi M, Babau JP, Schwarz JJ (2004) Temporal verification of real-time multitasking application properties based on communicating timed automata. In: Eighth IEEE international symposium on distributed simulation and real-time applications, 2004. DS-RT 2004, pp 188\u2013195","DOI":"10.1109\/DS-RT.2004.39"},{"issue":"3","key":"20_CR10","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1016\/j.jss.2011.05.022","volume":"85","author":"K Benghazi","year":"2012","unstructured":"Benghazi K, Hurtado MV, Hornos MJ, Rodr\u00edguez ML, Rodr\u00edguez-Dom\u00ednguez C, Pelegrina AB, Rodr\u00edguez-F\u00f3rtiz MJ (2012) Enabling correct design and formal analysis of ambient assisted living systems. J Syst Softw 85(3):498\u2013510","journal-title":"J Syst Softw"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Brush AB, Lee B, Mahajan R, Agarwal S, Saroiu S, Dixon C (2011) Home automation in the wild: challenges and opportunities. In: Proceedings of the SIGCHI conference on human factors in computing systems, ACM, New York, NY, USA, CHI \u201911, pp 2115\u20132124","DOI":"10.1145\/1978942.1979249"},{"issue":"4","key":"20_CR12","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1007\/s12652-013-0209-4","volume":"5","author":"F Corno","year":"2013","unstructured":"Corno F, Sanaullah M (2013) Design-time formal verification for smart environments: an exploratory perspective. J Ambient Intell Humaniz Comput 5(4):581\u2013599","journal-title":"J Ambient Intell Humaniz Comput"},{"key":"20_CR13","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1109\/MC.2010.335","volume":"43","author":"A Coronato","year":"2010","unstructured":"Coronato A, Pietro GD (2010) Formal design of ambient intelligence applications. Computer 43:60\u201368","journal-title":"Computer"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Dalsgaard P, Le Guilly T, Middelhede D, Olsen P, Pedersen T, Ravn A, Skou A (2013) A toolchain for home automation controller development. In: 2013 39th EUROMICRO conference on software engineering and advanced applications (SEAA), pp 122\u2013129","DOI":"10.1109\/SEAA.2013.36"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Davidoff S, Lee M, Yiu C, Zimmerman J, Dey A (2006) Principles of smart home control. In: UbiComp 2006: ubiquitous computing, lecture notes in computer science, pp 19\u201334","DOI":"10.1007\/11853565_2"},{"key":"20_CR16","unstructured":"Ericsson A (2009) Enabling tool support for formal analysis of eca rules. PhD thesis, Linkping UniversityLinkping University, Department of Computer and Information Science, The Institute of Technology"},{"issue":"12","key":"20_CR17","first-page":"1633","volume":"16","author":"M Garc\u00eda-Herranz","year":"2010","unstructured":"Garc\u00eda-Herranz M, Haya PA, Alam\u00e1n X (2010) Towards a ubiquitous end-user programming system for smart spaces. J UCS 16(12):1633\u20131649","journal-title":"J UCS"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Gruhn V, Laue R (2005) Specification patterns for time-related properties. In: 12th international symposium on temporal representation and reasoning, 2005. TIME 2005, pp 189\u2013191","DOI":"10.1109\/TIME.2005.33"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Guilly T, Olsen P, Pedersen T, Ravn AP, Skou A (2016) Software technologies: 10th international joint conference, ICSOFT 2015, Colmar, France, July 20\u201322, 2015, Revised Selected Papers, Springer International Publishing, Cham, chap Model Checking Feature Interactions, pp 307\u2013325","DOI":"10.1007\/978-3-319-30142-6_17"},{"issue":"8","key":"20_CR20","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8):666\u2013677","journal-title":"Commun ACM"},{"key":"20_CR21","unstructured":"Karagiannis T, Athanasopoulos E, Gkantsidis C, Key P (2008) Homemaestro: order from chaos in home networks. Tech. rep, Microsoft Research"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Le Guilly T, Olsen P, Ravn A, Rosenkilde J, Skou A (2013) HomePort: middleware for heterogeneous home automation networks. In: 2013 IEEE international conference on pervasive computing and communications workshops (PERCOM workshops), pp 627\u2013633","DOI":"10.1109\/PerComW.2013.6529570"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Le Guilly T, Olsen P, Ravn AP, Skou A (2015a) Modelling and analysis of component faults and reliability. In: Petre L, Sekerinski E (eds) From action system to distributed systems: the refinement approach. Taylor & Francis, Abingdon","DOI":"10.1201\/b20053-7"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Le Guilly T, Smedegard JH, Pedersen T, Skou A (2015b) To do and not to do: constrained scenarios for safe smart house. In: 2015 international conference on intelligent environments (IE), pp 17\u201324","DOI":"10.1109\/IE.2015.11"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Lee J, Gardu $$\\tilde{\\rm n}$$ n ~ o L, Walker E, Burleson W (2013) A tangible programming tool for creation of contextaware applications. In: Proceedings of the 2013 ACM international joint conference on pervasive and ubiquitous computing, UbiComp\u201913, pp 391\u2013400","DOI":"10.1145\/2493432.2493483"},{"key":"20_CR26","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime verification, lecture notes in computer science","author":"A Legay","year":"2010","unstructured":"Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace G, Rou G, Sokolsky O, Tillmann N (eds) Runtime verification, lecture notes in computer science, vol 6418. Springer, Berlin Heidelberg, pp 122\u2013135"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Liu Y, Zhang X, Dong JS, Liu Y, Sun J, Biswas J, Mokhtari M (2012) Formal analysis of pervasive computing systems. In: 2012 17th international conference on engineering of complex computer systems (ICECCS), pp 169\u2013178","DOI":"10.1109\/ICECCS20050.2012.6299212"},{"issue":"1","key":"20_CR28","first-page":"15","volume":"2","author":"SW Loe","year":"2008","unstructured":"Loe SW, Smanchat S, Ling S, Indrawan M (2008) Formal mirror models: an approach to just-in-time reasoning for device ecologies. Int J Smart Home 2(1):15\u201332","journal-title":"Int J Smart Home"},{"key":"20_CR29","volume-title":"Usability engineering","author":"J Nielsen","year":"1993","unstructured":"Nielsen J (1993) Usability engineering. Morgan Kaufmann Publishers Inc., San Francisco"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Pedersen T, Le Guilly T, Ravn A, Skou A (2015) A method for model checking feature interactions. In: Proceedings of the 10th international conference on software engineering and applications, pp 219\u2013228","DOI":"10.5220\/0005516402190228"},{"key":"20_CR31","unstructured":"Qiao Y, Wang H, Zhong K, Li X (2006) Visual event-condition-action rules with temporal events. In: Eighth real-time linux workshop, p 275"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Rogers Y (2006) Moving on from Weisers vision of calm computing: engaging ubicomp experiences. In: Dourish P, Friday A (eds) UbiComp 2006: ubiquitous computing, lecture notes in computer science, vol 4206. Springer, Berlin, pp 404\u2013421","DOI":"10.1007\/11853565_24"},{"key":"20_CR33","unstructured":"S\u00f8rensen MG (2014) Controller synthesis for home automation. Master\u2019s thesis, Department of Computer Science, Aalborg University"},{"key":"20_CR34","unstructured":"Thums A, Schellhorn G (2003) FME 2003: Formal methods: international symposium of formal methods Europe, Pisa, Italy, September 8\u201314, 2003. Proceedings, Springer, Berlin, Heidelberg, chap Model Checking FTA, pp 739\u2013757"},{"key":"20_CR35","doi-asserted-by":"crossref","unstructured":"Ur B, McManus E, Pak Yong Ho M, Littman ML (2014) Practical trigger-action programming in the smart home. In: Proceedings of the SIGCHI conference on human factors in computing systems, ACM, New York, NY, USA, CHI \u201914, pp 803\u2013812","DOI":"10.1145\/2556288.2557420"},{"key":"20_CR36","doi-asserted-by":"crossref","unstructured":"Valiente-Rocha P, Lozano-Tello A (2010) Ontology and SWRL-based learning model for home automation controlling. In: Ambient intelligence and future trends-international symposium on ambient intelligence (ISAm I 2010), advances in intelligent and soft computing, vol 72, pp 79\u201386","DOI":"10.1007\/978-3-642-13268-1_10"},{"issue":"3","key":"20_CR37","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1038\/scientificamerican0991-94","volume":"265","author":"M Weiser","year":"1991","unstructured":"Weiser M (1991) The computer for the 21st century. Sci Am 265(3):94\u2013104","journal-title":"Sci Am"}],"container-title":["Journal of Reliable Intelligent Environments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-016-0020-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s40860-016-0020-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-016-0020-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T11:46:58Z","timestamp":1600516018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s40860-016-0020-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5,4]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,7]]}},"alternative-id":["20"],"URL":"https:\/\/doi.org\/10.1007\/s40860-016-0020-z","relation":{},"ISSN":["2199-4668","2199-4676"],"issn-type":[{"value":"2199-4668","type":"print"},{"value":"2199-4676","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5,4]]}}}