{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:16:27Z","timestamp":1774984587079,"version":"3.50.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031751066","type":"print"},{"value":"9783031751073","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75107-3_21","type":"book-chapter","created":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T07:01:50Z","timestamp":1729926110000},"page":"351-367","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Local Reasoning and\u00a0Attribute-Based Memory Updates for\u00a0Enforcing Global Invariants in\u00a0Collective Adaptive Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9475-4836","authenticated-orcid":false,"given":"Michele","family":"Pasqua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0755-3444","authenticated-orcid":false,"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,27]]},"reference":[{"key":"21_CR1","first-page":"1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"Y Abd Alrahman","year":"2016","unstructured":"Abd Alrahman, Y., De Nicola, R., Loreti, M.: On the power of attribute-based communication. In: Albert, E., Lanese, I. (eds.) Formal Techniques for Distributed Objects, Components, and Systems, pp. 1\u201318. Springer, Cham (2016)"},{"key":"21_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102428","volume":"192","author":"Y Abd Alrahman","year":"2020","unstructured":"Abd Alrahman, Y., De Nicola, R., Loreti, M.: Programming interactions in collective adaptive systems by relying on attribute-based communication. Sci. Comput. Program. 192, 102428 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102428","journal-title":"Sci. Comput. Program."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Abd\u00a0Alrahman, Y., De Nicola, R., Loreti, M., Tiezzi, F., Vigo, R.: A calculus for attribute-based communication. In: Proceedings of 30th SAC, pp. 1840\u20131845. ACM (2015)","DOI":"10.1145\/2695664.2695668"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Aldini, A.: Design and verification of trusted collective adaptive systems. ACM Trans. Model. Comput. Simul. 28(2) (2018). https:\/\/doi.org\/10.1145\/3155337","DOI":"10.1145\/3155337"},{"issue":"4","key":"21_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","journal-title":"Inf. Process. Lett."},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Audrito, G., Damiani, F., Stolz, V., Viroli, M.: On distributed runtime verification by aggregate computing. In: Ancona, D., Pace, G. (eds.) Proceedings of the Second Workshop on Verification of Objects at RunTime EXecution. EPTCS, vol.\u00a0302, pp. 47\u201361 (2019). https:\/\/doi.org\/10.4204\/EPTCS.302.4","DOI":"10.4204\/EPTCS.302.4"},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1006\/jpdc.1995.1098","volume":"28","author":"O Babaoglu","year":"1995","unstructured":"Babaoglu, O., Raynal, M.: Specification and verification of dynamic properties in distributed computations. J. Parall. Distrib. Comput. 28(2), 173\u2013185 (1995). https:\/\/doi.org\/10.1006\/jpdc.1995.1098","journal-title":"J. Parall. Distrib. Comput."},{"key":"21_CR8","doi-asserted-by":"publisher","unstructured":"Bacci, G., Miculan, M.: Structural operational semantics for continuous state probabilistic processes. In: Proceedings of\u00a0CMCS. Lecture Notes in Computer Science, vol.\u00a07399, pp. 71\u201389. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32784-1_5","DOI":"10.1007\/978-3-642-32784-1_5"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Bacci, G., Miculan, M.: Structural operational semantics for continuous state stochastic transition systems. J. Comput. Syst. Sci. 81(5), 834\u2013858 (2015). https:\/\/doi.org\/10.1016\/J.JCSS.2014.12.003","DOI":"10.1016\/J.JCSS.2014.12.003"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Balliu, M., Merro, M., Pasqua, M., Shcherbakov, M.: Friendly fire: Cross-app interactions in IoT platforms. ACM Trans. Priv. Secur. 24(3) (2021). https:\/\/doi.org\/10.1145\/3444963","DOI":"10.1145\/3444963"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Bortolussi, L., et al.: CARMA: collective adaptive resource-sharing markovian agents. In: Proceedings of\u00a0QAPL 2015, pp. 16\u201331 (2015). https:\/\/doi.org\/10.4204\/eptcs.194.2","DOI":"10.4204\/eptcs.194.2"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Cano, J., Rutten, E., Delaval, G., Benazzouz, Y., Gurgen, L.: ECA rules for IoT environment: a case study in safe design. In: Proceedings of 8th SASOW, pp. 116\u2013121. IEEE, USA (2014). https:\/\/doi.org\/10.1109\/SASOW.2014.32","DOI":"10.1109\/SASOW.2014.32"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Lamport, L.: Distributed snapshots: dDetermining global states of a distributed system. ACM Trans. Comput. Syst. 3(1), 63\u201375 (1985)","DOI":"10.1145\/214451.214456"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Clarkson, M., Schneider, F.: Hyperproperties. In: 21st IEEE Computer Security Foundations Symposium, pp. 51\u201365 (2008). https:\/\/doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Francalanza, A., P\u00e9rez, J.A., S\u00e1nchez, C.: Runtime Verification for Decentralised and Distributed Systems, pp. 176\u2013210. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_6","DOI":"10.1007\/978-3-319-75632-5_6"},{"issue":"1","key":"21_CR16","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0378-7788(92)90047-K","volume":"18","author":"B Givoni","year":"1992","unstructured":"Givoni, B.: Comfort, climate analysis and building design guidelines. Energy Build. 18(1), 11\u201323 (1992)","journal-title":"Energy Build."},{"key":"21_CR17","doi-asserted-by":"publisher","unstructured":"Miculan, M., Pasqua, M.: A calculus for attribute-based memory updates. In: Cerone, A., \u00d6lveczky, P. (eds.) Proceedings of\u00a018th International Colloquium on Theoretical Aspects of Computing (ICTAC). Lecture Notes in Computer Science, vol. 12819, pp. 366\u2013385. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-85315-0_21","DOI":"10.1007\/978-3-030-85315-0_21"},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"132763","DOI":"10.1109\/ACCESS.2022.3230287","volume":"10","author":"M Pasqua","year":"2022","unstructured":"Pasqua, M., Comuzzo, M., Miculan, M.: The AbU language: IoT distributed programming made easy. IEEE Access 10, 132763\u2013132776 (2022). https:\/\/doi.org\/10.1109\/ACCESS.2022.3230287","journal-title":"IEEE Access"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Pasqua, M., Miculan, M.: On the security and safety of AbU systems. In: Proceedings of\u00a019th SEFM. Lecture Notes in Computer Science, vol. 13085, pp. 178\u2013198. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_11","DOI":"10.1007\/978-3-030-92124-8_11"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Pasqua, M., Miculan, M.: AbU: A calculus for distributed event-driven programming with attribute-based interaction. Theoretical Computer Science pp. 1\u201332 (2023). https:\/\/doi.org\/10.1016\/j.tcs.2023.113841","DOI":"10.1016\/j.tcs.2023.113841"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Pasqua, M., Miculan, M.: Behavioral equivalences for AbU: Verifying security and safety in distributed IoT systems. Theor. Comput. Sci. 998, 114537 (2024). https:\/\/doi.org\/10.1016\/j.tcs.2024.114537","DOI":"10.1016\/j.tcs.2024.114537"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75107-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T07:13:58Z","timestamp":1729926838000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75107-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,27]]},"ISBN":["9783031751066","9783031751073"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75107-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,27]]},"assertion":[{"value":"27 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}