{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:25Z","timestamp":1750306585332,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T00:00:00Z","timestamp":1443052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006435","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1302563"],"award-info":[{"award-number":["CNS-1302563"]}],"id":[{"id":"10.13039\/100006435","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,12,8]]},"abstract":"<jats:p>Cyber-physical systems (CPSs) may interact and manipulate objects in the physical world, and therefore formal guarantees about their behavior are strongly desired. Static-time proofs of safety invariants, however, may be intractable for systems with distributed physical-world interactions. This is further complicated when realistic communication models are considered, for which there may not be bounds on message delays, or even when considering that messages will eventually reach their destination.<\/jats:p>\n          <jats:p>In this work, we address the challenge of proving safety and progress in distributed CPSs communicating over an unreliable communication layer. We show that for this type of communication model, system safety is closely related to the results of a hybrid system\u2019s reachability computation, which can be computed at runtime. However, since computing reachability at runtime may be computationally intensive, we provide an approach that moves significant parts of the computation to design time. This approach is demonstrated with a case study of a simulation of multiple vehicles moving within a shared environment.<\/jats:p>","DOI":"10.1145\/2739046","type":"journal-article","created":{"date-parts":[[2015,9,29]],"date-time":"2015-09-29T19:22:29Z","timestamp":1443554549000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Safety and Progress for Distributed Cyber-Physical Systems with Unreliable Communication"],"prefix":"10.1145","volume":"14","author":[{"given":"Stanley","family":"Bak","sequence":"first","affiliation":[{"name":"United States Air Force Research Lab, Information Directorate"}]},{"given":"Zhenqi","family":"Huang","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]},{"given":"Fardin Abdi Taghi","family":"Abad","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]},{"given":"Marco","family":"Caccamo","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]}],"member":"320","published-online":{"date-parts":[[2015,9,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2013.6732229"},{"key":"e_1_2_1_2_1","volume-title":"ACM\/IEEE 16th International Conference on Hybrid Systems.","author":"Bak Stanley","year":"2013","unstructured":"Stanley Bak and Marco Caccamo. 2013. Computing reachability for nonlinear systems with hycreate. In Demo and Poster Session, ACM\/IEEE 16th International Conference on Hybrid Systems."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2009.20"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2014.21"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"K. Mani Chandy Sayan Mitra and Concetta Pilotto. 2008. Convergence verification: From shared memory to partially synchronous systems. In FORMATS. 218--232. 10.1007\/978-3-540-85778-5_16","DOI":"10.1007\/978-3-540-85778-5_16"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.70"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1338441.1338673"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032335"},{"key":"e_1_2_1_11_1","unstructured":"Honeywell. 2012. OneWireless Network - ISA100.11a-Compliant Wireless Mesh Network. Retrieved from https:\/\/www.honeywellprocess.com\/en-US\/explore\/products\/wireless\/OneWireless-Network\/pages\/default.aspx."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1203437"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795215"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2001.936213"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2008.15"},{"key":"e_1_2_1_17_1","first-page":"137","article-title":"On the stability of asynchronous iterative processes","volume":"20","author":"Tsitsiklis John N.","year":"1987","unstructured":"John N. Tsitsiklis. 1987. On the stability of asynchronous iterative processes. Theory of Computing Systems 20, 1 (1987), 137--153.","journal-title":"Theory of Computing Systems"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.153253"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2012.2219060"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2739046","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2739046","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:23Z","timestamp":1750227383000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2739046"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,24]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12,8]]}},"alternative-id":["10.1145\/2739046"],"URL":"https:\/\/doi.org\/10.1145\/2739046","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2015,9,24]]},"assertion":[{"value":"2014-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-02-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-24","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}