{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T20:05:35Z","timestamp":1760731535728,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>To support the dynamic composition of various devices\/apps into a medical\nsystem at point-of-care, a set of communication patterns to describe the\ncommunication needs of devices has been proposed. To address timing\nrequirements, each pattern breaks common timing properties into finer ones that\ncan be enforced locally by the components. Common timing requirements for the\nunderlying communication substrate are derived from these local properties. The\nlocal properties of devices are assured by the vendors at the development time.\nAlthough organizations procure devices that are compatible in terms of their\nlocal properties and middleware, they may not operate as desired. The latency\nof the organization network interacts with the local properties of devices. To\nvalidate the interaction among the timing properties of components and the\nnetwork, we formally specify such systems in Timed Rebeca. We use model\nchecking to verify the derived timing requirements of the communication\nsubstrate in terms of the network and device models. We provide a set of\ntemplates as a guideline to specify medical systems in terms of the formal\nmodel of patterns. A composite medical system using several devices is subject\nto state-space explosion. We extend the reduction technique of Timed Rebeca\nbased on the static properties of patterns. We prove that our reduction is\nsound and show the applicability of our approach in reducing the state space by\nmodeling two clinical scenarios made of several instances of patterns.<\/jats:p>","DOI":"10.46298\/lmcs-18(2:13)2022","type":"journal-article","created":{"date-parts":[[2022,6,8]],"date-time":"2022-06-08T14:51:39Z","timestamp":1654699899000},"source":"Crossref","is-referenced-by-count":3,"title":["Specification and Verification of Timing Properties in Interoperable Medical Systems"],"prefix":"10.46298","volume":"Volume 18, Issue 2","author":[{"given":"Mahsa","family":"Zarneshan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fatemeh","family":"Ghassemi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2022,6,1]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9639\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9639\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:18:58Z","timestamp":1687292338000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/6964"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,1]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(2:13)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2012.04025v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2012.04025v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2012.04025v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2012.04025v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2012.04025","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2012.04025","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,6,1]]},"article-number":"6964"}}