{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:47Z","timestamp":1775873627628,"version":"3.50.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["SHF 2211997, SHF 1749539"],"award-info":[{"award-number":["SHF 2211997, SHF 1749539"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>We develop a session types based framework for implementing and validating rate-based message passing systems in Internet of Things (IoT) domains. To model the indefinite repetition present in many embedded and IoT systems, we introduce a timed process calculus with a periodic recursion primitive. This allows us to model rate-based computations and communications inherent to these application domains. We introduce a definition of rate based session types in a binary session types setting and a new compatibility relationship, which we call rate compatibility. Programs which type check enjoy the standard session types guarantees as well as rate error freedom --- meaning processes which exchanges messages do so at the same rate. Rate compatibility is defined through a new notion of type expansion, a relation that allows communication between processes of differing periods by synthesizing and checking a common superperiod type. We prove type preservation and rate error freedom for our system, and show a decidable method for type checking based on computing superperiods for a collection of processes. We implement a prototype of our type system including rate compatibility via an embedding into the native type system of Rust. We apply this framework to a range of examples from our target domain such as Android software sensors, wearable devices, and sound processing.<\/jats:p>","DOI":"10.1145\/3622854","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1589-1617","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Validating IoT Devices with Rate-Based Session Types"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-4138-5001","authenticated-orcid":false,"given":"Grant","family":"Iraci","sequence":"first","affiliation":[{"name":"University at Buffalo, Buffalo, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3961-7118","authenticated-orcid":false,"given":"Cheng-En","family":"Chuang","sequence":"additional","affiliation":[{"name":"University at Buffalo, Buffalo, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4361-6772","authenticated-orcid":false,"given":"Raymond","family":"Hu","sequence":"additional","affiliation":[{"name":"Queen Mary University of London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4353-1998","authenticated-orcid":false,"given":"Lukasz","family":"Ziarek","sequence":"additional","affiliation":[{"name":"University at Buffalo, Buffalo, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2017.2657006"},{"key":"e_1_2_1_2_1","unstructured":"Android. 2009. Motion Sensors. https:\/\/developer.android.com\/guide\/topics\/sensors\/sensors_motion \t\t\t\t  Android. 2009. Motion Sensors. https:\/\/developer.android.com\/guide\/topics\/sensors\/sensors_motion"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"e_1_2_1_5_1","unstructured":"2023. Bluetooth Core Specification. 5.4 \t\t\t\t  2023. Bluetooth Core Specification. 5.4"},{"key":"e_1_2_1_6_1","volume-title":"Vasco Thudichum Vasconcelos, and Nobuko Yoshida","author":"Bocchi Laura","year":"2019","unstructured":"Laura Bocchi , Maurizio Murgia , Vasco Thudichum Vasconcelos, and Nobuko Yoshida . 2019 . Asynchronous Timed Session Types. In Programming Languages and Systems, Lu\u00eds Caires (Ed.). Springer International Publishing , Cham. 583\u2013610. isbn:978-3-030-17184-1 Laura Bocchi, Maurizio Murgia, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2019. Asynchronous Timed Session Types. In Programming Languages and Systems, Lu\u00eds Caires (Ed.). Springer International Publishing, Cham. 583\u2013610. isbn:978-3-030-17184-1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_29"},{"key":"e_1_2_1_8_1","unstructured":"Richard R. Brooks and S. S. Iyengar. 1998. Multi-Sensor Fusion: Fundamentals and Applications with Software. Prentice-Hall Inc. USA. isbn:0139016538 \t\t\t\t  Richard R. Brooks and S. S. Iyengar. 1998. Multi-Sensor Fusion: Fundamentals and Applications with Software. Prentice-Hall Inc. USA. isbn:0139016538"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.22"},{"key":"e_1_2_1_11_1","volume-title":"Wyglinski","author":"Collins Travis F.","year":"2018","unstructured":"Travis F. Collins , Robin Getz , Di Pu , and Alexander M . Wyglinski . 2018 . Software-Defined Radio for Engineers. Artech House . https:\/\/www.analog.com\/en\/education\/education-library\/software-defined-radio-for-engineers.html Travis F. Collins, Robin Getz, Di Pu, and Alexander M. Wyglinski. 2018. Software-Defined Radio for Engineers. Artech House. https:\/\/www.analog.com\/en\/education\/education-library\/software-defined-radio-for-engineers.html"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236786"},{"key":"e_1_2_1_13_1","unstructured":"FreeRTOS. 2003. FreeRTOS Kernel. https:\/\/www.freertos.org\/ \t\t\t\t  FreeRTOS. 2003. FreeRTOS Kernel. https:\/\/www.freertos.org\/"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_2_1_15_1","volume-title":"CONCUR\u201993","author":"Honda Kohei","unstructured":"Kohei Honda . 1993. Types for dyadic interaction . In CONCUR\u201993 , Eike Best (Ed.). Springer Berlin Heidelberg, Berlin , Heidelberg . 509\u2013523. isbn:978-3-540-47968-0 Kohei Honda. 1993. Types for dyadic interaction. In CONCUR\u201993, Eike Best (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 509\u2013523. isbn:978-3-540-47968-0"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580415"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808098.2808100"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/JIOT.2017.2683200"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.141"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12652-016-0350-y"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12599-021-00689-w"},{"key":"e_1_2_1_25_1","volume-title":"Practical Session Types in Rust. Master\u2019s thesis. Department of Computer Science","author":"Munksgaard Philip","unstructured":"Philip Munksgaard and Thomas Bracht Laumann Jespersen . 2015. Practical Session Types in Rust. Master\u2019s thesis. Department of Computer Science , University of Copenhagen. Philip Munksgaard and Thomas Bracht Laumann Jespersen. 2015. Practical Session Types in Rust. Master\u2019s thesis. Department of Computer Science, University of Copenhagen."},{"key":"e_1_2_1_26_1","unstructured":"Benjamin C. Pierce. 2002. The MIT Press 311\u2013312. \t\t\t\t  Benjamin C. Pierce. 2002. The MIT Press 311\u2013312."},{"key":"e_1_2_1_27_1","unstructured":"Pine64. 2019. PineTime. https:\/\/www.pine64.org\/pinetime\/ \t\t\t\t  Pine64. 2019. PineTime. https:\/\/www.pine64.org\/pinetime\/"},{"key":"e_1_2_1_28_1","unstructured":"QNX. 2001. QNX Neutrino. https:\/\/www.qnx.com\/products\/intl\/neutrino_rtos\/ \t\t\t\t  QNX. 2001. QNX Neutrino. https:\/\/www.qnx.com\/products\/intl\/neutrino_rtos\/"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2018.2873186"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.3390\/s19030477"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80382-2"},{"key":"e_1_2_1_33_1","unstructured":"Antonio Vallecillo Vasco T Vasconcelos and Antonio Ravara. 2006. Typing the Behavior of Software Components using Session Types. 16. \t\t\t\t  Antonio Vallecillo Vasco T Vasconcelos and Antonio Ravara. 2006. Typing the Behavior of Software Components using Session Types. 16."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364568"},{"key":"e_1_2_1_35_1","unstructured":"Pete Warden. 2020. TinyML: Machine learning with tensorflow on Arduino and ultra-low Power Micro-controllers. O\u2019REILLY MEDIA. \t\t\t\t  Pete Warden. 2020. TinyML: Machine learning with tensorflow on Arduino and ultra-low Power Micro-controllers. O\u2019REILLY MEDIA."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00449-012-0848-4"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.13154\/tches.v2019.i3.66-85"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2008.04.002"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622854","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622854"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":39,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622854"],"URL":"https:\/\/doi.org\/10.1145\/3622854","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}