{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:24:49Z","timestamp":1759638289951,"version":"3.41.0"},"reference-count":12,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2011,2,1]],"date-time":"2011-02-01T00:00:00Z","timestamp":1296518400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Auton. Adapt. Syst."],"published-print":{"date-parts":[[2011,2]]},"abstract":"<jats:p>This article presents a methodology to formally express requirements in safety-critical ubiquitous and pervasive applications in order to achieve a higher degree of dependability. In particular, it will be shown how it is possible to formalize and constrict mobility characteristics by combining and extending several formal methods. The article also discusses some issues concerning both static and dynamic verification.<\/jats:p>","DOI":"10.1145\/1921641.1921650","type":"journal-article","created":{"date-parts":[[2011,2,22]],"date-time":"2011-02-22T13:07:33Z","timestamp":1298380053000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Formal Specification and Verification of Ubiquitous and Pervasive Systems"],"prefix":"10.1145","volume":"6","author":[{"given":"Antonio","family":"Coronato","sequence":"first","affiliation":[{"name":"ICAR-CNR"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"De Pietro","sequence":"additional","affiliation":[{"name":"ICAR-CNR"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.007"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00231-5"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325742"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00832-0"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1814539.1814551"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1083246.1083249"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_2_2_9_1","first-page":"1","article-title":"Formal verification of component-based designs","volume":"11","author":"Karlsson D.","year":"2007","journal-title":"J. Des. Autom. Embedd. Syst."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.991322"},{"volume-title":"Proceedings of the 8th IEEE Real-Time Systems Symposium.","author":"Ostroff J. S.","key":"e_1_2_2_11_1"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-6205-y"}],"container-title":["ACM Transactions on Autonomous and Adaptive Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921641.1921650","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1921641.1921650","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:08Z","timestamp":1750278368000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921641.1921650"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,2]]},"references-count":12,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,2]]}},"alternative-id":["10.1145\/1921641.1921650"],"URL":"https:\/\/doi.org\/10.1145\/1921641.1921650","relation":{},"ISSN":["1556-4665","1556-4703"],"issn-type":[{"type":"print","value":"1556-4665"},{"type":"electronic","value":"1556-4703"}],"subject":[],"published":{"date-parts":[[2011,2]]},"assertion":[{"value":"2009-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}