{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T15:44:15Z","timestamp":1762875855447},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,2,27]],"date-time":"2017-02-27T00:00:00Z","timestamp":1488153600000},"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":["J Reliable Intell Environ"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s40860-017-0036-z","type":"journal-article","created":{"date-parts":[[2017,2,27]],"date-time":"2017-02-27T02:16:55Z","timestamp":1488161815000},"page":"117-130","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Symbolic verification of event\u2013condition\u2013action rules in intelligent environments"],"prefix":"10.1007","volume":"3","author":[{"given":"Claudia","family":"Vannucchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michelangelo","family":"Diamanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianmarco","family":"Mazzante","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diletta","family":"Cacciagrano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rosario","family":"Culmone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikos","family":"Gorogiannis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Mostarda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Raimondi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,27]]},"reference":[{"key":"36_CR1","unstructured":"Barrett C, Stump A, Tinelli C, Boehme S, Cok D, Deharbe D, Dutertre B, Fontaine P, Ganesh V, Griggio A, Grundy J, Jackson P, Oliveras A, Krsti\u00e4g S, Moskal M, Moura LD, Sebastiani R, Cok TD, Hoenicke JC (2010) The SMT-LIB standard: version 2.0. In: Technical report, Department of Computer Science, The University of Iowa"},{"key":"36_CR2","doi-asserted-by":"publisher","unstructured":"Berndtsson M, Mellin J (2009) ECA rules, pp 959\u2013960. Springer, Boston. doi:\n                        10.1007\/978-0-387-39940-9_504","DOI":"10.1007\/978-0-387-39940-9_504"},{"key":"36_CR3","doi-asserted-by":"publisher","unstructured":"Beyer D, Stahlbauer A (2014) BDD-based software verification. Int J Softw Tools Technol Transf 16(5):507\u2013518. doi:\n                        10.1007\/s10009-014-0334-1","DOI":"10.1007\/s10009-014-0334-1"},{"key":"36_CR4","unstructured":"Beyer D, Wendler P (2012) Algorithms for software model checking: predicate abstraction vs. impact. In: 2012 formal methods in computer-aided design (FMCAD), pp 106\u2013113"},{"key":"36_CR5","doi-asserted-by":"publisher","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691. doi:\n                        10.1109\/TC.1986.1676819","DOI":"10.1109\/TC.1986.1676819"},{"key":"36_CR6","doi-asserted-by":"publisher","unstructured":"Cano J, Delaval G, Rutten E (2014) Coordination models and languages. In: 16th IFIP WG 6.1 international conference, coordination 2014, held as part of the 9th international federated conferences on distributed computing techniques, DisCoTec 2014, Berlin, 3\u20135 June 2014. Proceedings, chapter Coordination of ECA rules by verification and control, pp 33\u201348. Springer, Berlin. doi:\n                        10.1007\/978-3-662-43376-8_3","DOI":"10.1007\/978-3-662-43376-8_3"},{"key":"36_CR7","doi-asserted-by":"publisher","unstructured":"Corradini F, Culmone R, Mostarda L, Tesei L, Raimondi F (2015) A constrained ECA language supporting formal verification of WSNs. In: 29th IEEE international conference on advanced information networking and applications workshops, AINA 2015 workshops, Gwangju, 24\u201327 March 2015, pp 187\u2013192. doi:\n                        10.1109\/WAINA.2015.109","DOI":"10.1109\/WAINA.2015.109"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS\u201908\/ETAPS\u201908, pp 337\u2013340. Springer, Berlin. \n                        http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2009) Satisfiability modulo theories: an appetizer. In: Brazilian symposium on formal methods, pp 23\u201336. Springer, New York","DOI":"10.1007\/978-3-642-10452-7_3"},{"issue":"4","key":"36_CR10","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s10626-013-0163-5","volume":"23","author":"G Delaval","year":"2013","unstructured":"Delaval G, Rutten E, Marchand H (2013) Integrating discrete controller synthesis into a reactive programming language compiler. Discrete Event Dyn Syst 23(4):385\u2013418. doi:\n                        10.1007\/s10626-013-0163-5","journal-title":"Discrete Event Dyn Syst"},{"key":"36_CR11","doi-asserted-by":"publisher","unstructured":"Dijkstra EW (1975) Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18(8):453\u2013457. doi:\n                        10.1145\/360933.360975","DOI":"10.1145\/360933.360975"},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"Dumas M, Hofstede AHMT (2001) UML activity diagrams as a workflow specification language. In: Proceedings of the fourth international conference on the unified modeling language, modeling languages, concepts, and tools. Springer, London, pp 76\u201390. \n                        http:\/\/dl.acm.org\/citation.cfm?id=647245.719456","DOI":"10.1007\/3-540-45441-1_7"},{"key":"36_CR13","unstructured":"Ericsson A (2009) Enabling tool support for formal analysis of ECA rules. Ph.D. thesis, University of Sk\u00f6vde"},{"key":"36_CR14","volume-title":"The science of programming. Monographs in computer science","author":"D Gries","year":"1989","unstructured":"Gries D (1989) The science of programming. Monographs in computer science. Springer, New York"},{"key":"36_CR15","unstructured":"Gu T, Wang XH, Pung HK, Zhang DQ (2004) An ontology-based context model in intelligent environments. In: Proceedings of communication networks and distributed systems modeling and simulation conference, vol 2004, San Diego, pp 270\u2013275"},{"key":"36_CR16","unstructured":"Jin X, Lembachar Y, Ciardo G (2013) Symbolic verification of ECA rules. In: Joint proceedings of the international workshop on petri nets and software engineering (PNSE\u201913) and the international workshop on modeling and business environments (ModBE\u201913), Milano, 24\u201325 June 2013, pp 41\u201359. \n                        http:\/\/ceur-ws.org\/Vol-989\/paper17.pdf"},{"key":"36_CR17","doi-asserted-by":"crossref","unstructured":"Lee WS, Lee SY, Lee KC (2007) Conflict detection and resolution method in WS-ECA framework. In: The 9th international conference on advanced communication technology, vol 1, pp 786\u2013791. IEEE, New York","DOI":"10.1109\/ICACT.2007.358468"},{"key":"36_CR18","doi-asserted-by":"publisher","unstructured":"Marchand H, Bournai P, Borgne ML, Guernic PL (2000) Synthesis of discrete-event controllers based on the signal environment. Discrete Event Dyn Syst 10(4):325\u2013346. doi:\n                        10.1023\/A:1008311720696","DOI":"10.1023\/A:1008311720696"},{"key":"36_CR19","doi-asserted-by":"crossref","unstructured":"Mostarda L, Marinovic S, Dulay N (2010) Distributed orchestration of pervasive services. In: 24th IEEE IAINA 2010, Perth, 13\u201320 April 2010, pp 166\u2013173","DOI":"10.1109\/AINA.2010.100"},{"issue":"2","key":"36_CR20","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/THMS.2014.2364613","volume":"45","author":"Y Sun","year":"2015","unstructured":"Sun Y, Wang X, Luo H, Li X (2015) Conflict detection scheme based on formal rule model for smart building systems. IEEE Trans Hum Mach Syst 45(2):215\u2013227. doi:\n                        10.1109\/THMS.2014.2364613","journal-title":"IEEE Trans Hum Mach Syst"},{"key":"36_CR21","doi-asserted-by":"publisher","unstructured":"Vannucchi C, Cacciagrano DR, Corradini F, Culmone R, Mostarda L, Raimondi F, Tesei L (2016) A formal model for event-condition-action rules in intelligent environments. In: Proceedings of the 11th international conference on intelligent environments, pp 56\u201365. doi:\n                        10.3233\/978-1-61499-690-3-56","DOI":"10.3233\/978-1-61499-690-3-56"},{"key":"36_CR22","doi-asserted-by":"publisher","unstructured":"Whitmore A, Agarwal A, Da Xu L (2015) The internet of things\u2014a survey of topics and trends. Inf Syst Front 17(2):261\u2013274. doi:\n                        10.1007\/s10796-014-9489-2","DOI":"10.1007\/s10796-014-9489-2"},{"key":"36_CR23","doi-asserted-by":"publisher","unstructured":"Yoon JP (1989) Techniques for data and rule validation in knowledge based systems. In: Computer assurance, 1989. In: Proceedings of the fourth annual conference on COMPASS \u201989, \u2019systems integrity, software safety and process security\u2019, pp 62\u201370. doi:\n                        10.1109\/CMPASS.1989.76042","DOI":"10.1109\/CMPASS.1989.76042"},{"key":"36_CR24","doi-asserted-by":"publisher","unstructured":"Zhang J, Moyne J, Tilbury D (2008) Verification of ECA rule based management and control systems. In: 2008 IEEE international conference on automation science and engineering, pp 1\u20137. doi:\n                        10.1109\/COASE.2008.4626431","DOI":"10.1109\/COASE.2008.4626431"}],"container-title":["Journal of Reliable Intelligent Environments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s40860-017-0036-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-017-0036-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-017-0036-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,5]],"date-time":"2017-07-05T10:05:57Z","timestamp":1499249157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s40860-017-0036-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,27]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["36"],"URL":"https:\/\/doi.org\/10.1007\/s40860-017-0036-z","relation":{},"ISSN":["2199-4668","2199-4676"],"issn-type":[{"value":"2199-4668","type":"print"},{"value":"2199-4676","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,27]]}}}