{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T12:51:58Z","timestamp":1777380718733,"version":"3.51.4"},"reference-count":33,"publisher":"SAGE Publications","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIS"],"published-print":{"date-parts":[[2018,6,21]]},"DOI":"10.3233\/ais-180487","type":"journal-article","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T12:47:32Z","timestamp":1529066852000},"page":"261-273","source":"Crossref","is-referenced-by-count":6,"title":["Analysis and verification of ECA rules in intelligent environments"],"prefix":"10.1177","volume":"10","author":[{"given":"Diletta Romana","family":"Cacciagrano","sequence":"first","affiliation":[{"name":"Computer Science Division, University of Camerino, Camerino, Italy. E-mails:\u00a0diletta.cacciagrano@unicam.it,\u00a0flavio.corradini@unicam.it,\u00a0rosario.culmone@unicam.it,\u00a0leonardo.mostarda@unicam.it,\u00a0claudia.vannucchi@unicam.it"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Flavio","family":"Corradini","sequence":"additional","affiliation":[{"name":"Computer Science Division, University of Camerino, Camerino, Italy. E-mails:\u00a0diletta.cacciagrano@unicam.it,\u00a0flavio.corradini@unicam.it,\u00a0rosario.culmone@unicam.it,\u00a0leonardo.mostarda@unicam.it,\u00a0claudia.vannucchi@unicam.it"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rosario","family":"Culmone","sequence":"additional","affiliation":[{"name":"Computer Science Division, University of Camerino, Camerino, Italy. E-mails:\u00a0diletta.cacciagrano@unicam.it,\u00a0flavio.corradini@unicam.it,\u00a0rosario.culmone@unicam.it,\u00a0leonardo.mostarda@unicam.it,\u00a0claudia.vannucchi@unicam.it"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikos","family":"Gorogiannis","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Middlesex University, London, UK. E-mails:\u00a0n.gkorogiannis@mdx.ac.uk,\u00a0f.raimondi@mdx.ac.uk"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Mostarda","sequence":"additional","affiliation":[{"name":"Computer Science Division, University of Camerino, Camerino, Italy. E-mails:\u00a0diletta.cacciagrano@unicam.it,\u00a0flavio.corradini@unicam.it,\u00a0rosario.culmone@unicam.it,\u00a0leonardo.mostarda@unicam.it,\u00a0claudia.vannucchi@unicam.it"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Raimondi","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Middlesex University, London, UK. E-mails:\u00a0n.gkorogiannis@mdx.ac.uk,\u00a0f.raimondi@mdx.ac.uk"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudia","family":"Vannucchi","sequence":"additional","affiliation":[{"name":"Computer Science Division, University of Camerino, Camerino, Italy. E-mails:\u00a0diletta.cacciagrano@unicam.it,\u00a0flavio.corradini@unicam.it,\u00a0rosario.culmone@unicam.it,\u00a0leonardo.mostarda@unicam.it,\u00a0claudia.vannucchi@unicam.it"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"issue":"6","key":"10.3233\/AIS-180487_ref1","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","article-title":"Binary decision diagrams","volume":"100","author":"Akers","year":"1978","journal-title":"IEEE Transactions on computers"},{"issue":"1","key":"10.3233\/AIS-180487_ref2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s40860-015-0005-3","article-title":"Introduction to the inaugural issue of the Journal of Reliable Intelligent Environments","volume":"1","author":"Augusto","year":"2015","journal-title":"Journal of Reliable Intelligent Environments"},{"key":"10.3233\/AIS-180487_ref3","unstructured":"J.C.\u00a0Augusto and M.J.\u00a0Hornos, Using simulation and verification to inform the development of intelligent environments, in: Intelligent Environments (Workshops), 2012, pp.\u00a0413\u2013424."},{"issue":"2","key":"10.3233\/AIS-180487_ref5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1109\/TNB.2007.897492","article-title":"An agent-based multilayer architecture for bioinformatics grids","volume":"6","author":"Bartocci","year":"2007","journal-title":"IEEE Transactions on Nanobioscience"},{"key":"10.3233\/AIS-180487_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020949"},{"key":"10.3233\/AIS-180487_ref7","doi-asserted-by":"crossref","unstructured":"M.\u00a0Berndtsson and J.\u00a0Mellin, ECA rules, in: Encyclopedia of Database Systems, L.\u00a0Liu and M.T.\u00a0\u00d6zsu, eds, Springer US, 2009, pp.\u00a0959\u2013960.","DOI":"10.1007\/978-0-387-39940-9_504"},{"issue":"5","key":"10.3233\/AIS-180487_ref8","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10009-014-0334-1","article-title":"BDD-based software verification","volume":"16","author":"Beyer","year":"2014","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.3233\/AIS-180487_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_28"},{"issue":"3","key":"10.3233\/AIS-180487_ref10","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1023\/B:BTTJ.0000047137.42670.4d","article-title":"Inhabited intelligent environments","volume":"22","author":"Callaghan","year":"2004","journal-title":"BT Technology Journal"},{"key":"10.3233\/AIS-180487_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43376-8_3"},{"issue":"6","key":"10.3233\/AIS-180487_ref12","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1145\/2499370.2491969","article-title":"Reasoning about nondeterminism in programs","volume":"48","author":"Cook","year":"2013","journal-title":"ACM SIGPLAN Notices"},{"key":"10.3233\/AIS-180487_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_37"},{"key":"10.3233\/AIS-180487_ref14","doi-asserted-by":"crossref","unstructured":"B.\u00a0Cook, A.\u00a0See and F.\u00a0Zuleger, Ramsey vs. lexicographic termination proving, in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2013, pp.\u00a047\u201361.","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"10.3233\/AIS-180487_ref15","doi-asserted-by":"publisher","DOI":"10.1109\/WAINA.2015.109"},{"key":"10.3233\/AIS-180487_ref16","doi-asserted-by":"crossref","unstructured":"L.\u00a0De Moura and N.\u00a0Bj\u00f8rner, Z3: An efficient SMT solver, in: Proceedings of the Theory and Practice of Software, 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908\/ETAPS\u201908, 2008, pp.\u00a0337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10.3233\/AIS-180487_ref17","doi-asserted-by":"crossref","unstructured":"L.\u00a0De Moura and N.\u00a0Bj\u00f8rner, Satisfiability modulo theories: An appetizer, in: Brazilian Symposium on Formal Methods, Springer, 2009, pp.\u00a023\u201336.","DOI":"10.1007\/978-3-642-10452-7_3"},{"issue":"4","key":"10.3233\/AIS-180487_ref18","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s10626-013-0163-5","article-title":"Integrating discrete controller synthesis into a reactive programming language compiler","volume":"23","author":"Delaval","year":"2013","journal-title":"Discrete Event Dynamic Systems"},{"issue":"8","key":"10.3233\/AIS-180487_ref19","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded commands, nondeterminacy and formal derivation of programs","volume":"18","author":"Dijkstra","year":"1975","journal-title":"Commun. ACM"},{"key":"10.3233\/AIS-180487_ref21","unstructured":"D.\u00a0Gries, The Science of Programming, Monographs in Computer Science, Springer, 1989."},{"key":"10.3233\/AIS-180487_ref22","unstructured":"X.\u00a0Jin, Y.\u00a0Lembachar and G.\u00a0Ciardo, Symbolic verification of ECA rules, in: Joint Proc. of the Int. Workshop on Petri Nets and Software Eng. and the Int. Workshop on Modeling and Business Env. (ModBE\u201913), 2013, pp.\u00a041\u201359."},{"issue":"6","key":"10.3233\/AIS-180487_ref23","doi-asserted-by":"publisher","first-page":"33","DOI":"10.5121\/ijcnc.2012.4603","article-title":"Intelligent home monitoring using RSSI in wireless sensor networks","volume":"4","author":"Kausar","year":"2012","journal-title":"International Journal of Computer Networks & Communications"},{"issue":"3","key":"10.3233\/AIS-180487_ref24","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s11047-014-9436-7","article-title":"Topology driven modeling: The IS metaphor","volume":"14","author":"Merelli","year":"2015","journal-title":"Natural Computing"},{"issue":"10","key":"10.3233\/AIS-180487_ref25","doi-asserted-by":"publisher","first-page":"6872","DOI":"10.3390\/e17106872","article-title":"Topological characterization of complex systems: Using persistent entropy","volume":"17","author":"Merelli","year":"2015","journal-title":"Entropy"},{"key":"10.3233\/AIS-180487_ref26","doi-asserted-by":"crossref","unstructured":"L.\u00a0Mostarda, S.\u00a0Marinovic and N.\u00a0Dulay, Distributed orchestration of pervasive services, in: 24th IEEE IAINA 2010, Perth, Australia, 20\u201313 April 2010, 2010, pp.\u00a0166\u2013173.","DOI":"10.1109\/AINA.2010.100"},{"issue":"4","key":"10.3233\/AIS-180487_ref27","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","article-title":"Petri nets: Properties, analysis and applications","volume":"77","author":"Murata","year":"1989","journal-title":"Proceedings of the IEEE"},{"key":"10.3233\/AIS-180487_ref28","doi-asserted-by":"crossref","unstructured":"G.J.\u00a0Myers, C.\u00a0Sandler and T.\u00a0Badgett, The Art of Software Testing, John Wiley & Sons, 2011.","DOI":"10.1002\/9781119202486"},{"key":"10.3233\/AIS-180487_ref29","doi-asserted-by":"crossref","unstructured":"D.\u00a0Preuveneers and W.\u00a0Joosen, Change impact analysis for context-aware applications in intelligent environments, in: Intelligent Environments, 2015.","DOI":"10.3233\/978-1-61499-530-2-70"},{"issue":"2","key":"10.3233\/AIS-180487_ref30","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","article-title":"Finite automata and their decision problems","volume":"3","author":"Rabin","year":"1959","journal-title":"IBM journal of research and development"},{"issue":"4","key":"10.3233\/AIS-180487_ref31","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1016\/j.jss.2010.10.023","article-title":"A policy-based publish\/subscribe middleware for sense-and-react applications","volume":"84","author":"Russello","year":"2011","journal-title":"Journal of Systems and Software"},{"key":"10.3233\/AIS-180487_ref32","unstructured":"K.\u00a0Schneider, Verification of Reactive Systems: Formal Methods and Algorithms, Springer Verlag, 2004, ISBN 3540002960."},{"issue":"2","key":"10.3233\/AIS-180487_ref33","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/THMS.2014.2364613","article-title":"Conflict detection scheme based on formal rule model for smart building systems","volume":"45","author":"Sun","year":"2015","journal-title":"IEEE Transactions on Human\u2013Machine Systems"},{"key":"10.3233\/AIS-180487_ref34","unstructured":"C.\u00a0Vannucchi, D.R.\u00a0Cacciagrano, F.\u00a0Corradini, R.\u00a0Culmone, L.\u00a0Mostarda, F.\u00a0Raimondi and L.\u00a0Tesei, A Formal Model for Event\u2013Condition\u2013Action Rules in Intelligent Environments, in: Proceedings of the 11th International Conference on Intelligent Environments, 2016, pp.\u00a056\u201365."},{"key":"10.3233\/AIS-180487_ref35","doi-asserted-by":"crossref","unstructured":"C.\u00a0Vannucchi, D.R.\u00a0Cacciagrano, R.\u00a0Culmone and L.\u00a0Mostarda, Towards a uniform ontology-driven approach for modeling, checking and executing WSANs, in: 2016 30th International Conference on Advanced Information Networking and Applications Workshops (WAINA), 2016, pp.\u00a0319\u2013324.","DOI":"10.1109\/WAINA.2016.79"}],"container-title":["Journal of Ambient Intelligence and Smart Environments"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIS-180487","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T09:18:37Z","timestamp":1777367917000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIS-180487"}},"subtitle":[],"editor":[{"given":"Jason J.","family":"Jung","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"Paulo","family":"Novais","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2018,6,21]]},"references-count":33,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.3233\/ais-180487","relation":{},"ISSN":["1876-1372","1876-1364"],"issn-type":[{"value":"1876-1372","type":"electronic"},{"value":"1876-1364","type":"print"}],"subject":[],"published":{"date-parts":[[2018,6,21]]}}}