{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,18]],"date-time":"2025-09-18T10:31:40Z","timestamp":1758191500110,"version":"3.44.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"crossref","award":["2211997, 1749539"],"award-info":[{"award-number":["2211997, 1749539"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n            We develop a session types 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\n            <jats:italic toggle=\"yes\">rate-based<\/jats:italic>\n            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\n            <jats:italic toggle=\"yes\">rate compatibility<\/jats:italic>\n            . Programs which type-check enjoy the standard session types guarantees as well as rate error freedom\u2014meaning processes which exchanges messages do so at the same\n            <jats:italic toggle=\"yes\">rate<\/jats:italic>\n            . 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\n            <jats:italic toggle=\"yes\">rate error freedom<\/jats:italic>\n            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. Our framework is used to implement a heart rate sensor application that runs on a commercially available smartwatch.\n          <\/jats:p>","DOI":"10.1145\/3754449","type":"journal-article","created":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T17:12:49Z","timestamp":1753377169000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Rate-Based Session Types for IoT Systems"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-4138-5001","authenticated-orcid":false,"given":"Grant","family":"Iraci","sequence":"first","affiliation":[{"name":"University at Buffalo, Buffalo, New York, 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, New York, 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, New York, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,9,17]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"AbsInt. 2002. aiT worst-case execution time analyzers. aiT. Retrieved from https:\/\/www.absint.com\/ait\/"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"Kazi Masudul Alam and Abdulmotaleb El Saddik. 2017. C2PS: A digital twin architecture reference model for the cloud-based cyber-physical systems. IEEE Access 5 (2017) 2050\u20132062. DOI: 10.1109\/ACCESS.2017.2657006","DOI":"10.1109\/ACCESS.2017.2657006"},{"key":"e_1_3_2_4_1","unstructured":"Android. 2009. Motion sensors. Retrieved from https:\/\/developer.android.com\/guide\/topics\/sensors\/sensors_motion"},{"key":"e_1_3_2_5_1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"1","author":"Balzer Stephanie","year":"2017","unstructured":"Stephanie Balzer and Frank Pfenning. 2017. Manifest sharing with session types. Proceedings of the ACM on Programming Languages 1, ICFP, Article 37 (Aug. 2017), 29 pages. DOI: 10.1145\/3110281"},{"key":"e_1_3_2_6_1","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/REAL.2002.1181582","volume-title":"Proceedings of the 23rd IEEE Real-Time Systems Symposium, 2002 (RTSS \u201902).","author":"Bernat G.","year":"2002","unstructured":"G. Bernat, A. Colin, and S.M. Petters. 2002. WCET analysis of probabilistic hard real-time systems. In Proceedings of the 23rd IEEE Real-Time Systems Symposium, 2002 (RTSS \u201902). IEEE, 279\u2013288. DOI: 10.1109\/REAL.2002.1181582"},{"key":"e_1_3_2_7_1","first-page":"418","volume-title":"Proceedings of the 19th International Conference on Concurrency Theory (CONCUR \u201908)Lecture Notes in Computer Science","volume":"5201","author":"Bettini Lorenzo","year":"2008","unstructured":"Lorenzo Bettini, Mario Coppo, Loris D\u2019Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2008. Global progress in dynamically interleaved multiparty sessions. In Proceedings of the 19th International Conference on Concurrency Theory (CONCUR \u201908). Franck van Breugel and Marsha Chechik (Eds.), Lecture Notes in Computer Science, Vol. 5201, Springer, 418\u2013433. DOI: 10.1007\/978-3-540-85361-9_33"},{"key":"e_1_3_2_8_1","unstructured":"Bluetooth SIG 2023. Bluetooth Core Specification 5.4. Bluetooth SIG."},{"key":"e_1_3_2_9_1","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/978-3-030-17184-1_21","volume-title":"Programming Languages and Systems","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."},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_29"},{"key":"e_1_3_2_11_1","volume-title":"Multi-Sensor Fusion: Fundamentals and Applications with Software","author":"Brooks Richard R.","year":"1998","unstructured":"Richard R. Brooks and S. S. Iyengar. 1998. Multi-Sensor Fusion: Fundamentals and Applications with Software. Prentice-Hall, Inc."},{"key":"e_1_3_2_12_1","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"Concurrency Theory (CONCUR \u201910)","author":"Caires Lu\u00eds","year":"2010","unstructured":"Lu\u00eds Caires and Frank Pfenning. 2010. Session types as intuitionistic linear propositions. In Concurrency Theory (CONCUR \u201910). Paul Gastin and Fran\u00e7ois Laroussinie (Eds.), Springer, Berlin, 222\u2013236."},{"key":"e_1_3_2_13_1","first-page":"22:1","volume-title":"Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP \u201922)Leibniz International Proceedings in Informatics (LIPIcs)","volume":"222","author":"Chen Ruo Fei","year":"2022","unstructured":"Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho. 2022. Ferrite: A judgmental embedding of session types in rust. In Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP \u201922). Karim Ali and Jan Vitek (Eds.), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 222, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 22:1\u201322:28. DOI: 10.4230\/LIPIcs.ECOOP.2022.22"},{"key":"e_1_3_2_14_1","volume-title":"Software-Defined Radio for Engineers","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. Retrieved from https:\/\/www.analog.com\/en\/education\/education-library\/software-defined-radio-for-engineers.html"},{"key":"e_1_3_2_15_1","first-page":"246","volume-title":"Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming(PPoPP \u201922)","author":"Cutner Zak","year":"2022","unstructured":"Zak Cutner, Nobuko Yoshida, and Martin Vassor. 2022. Deadlock-free asynchronous message reordering in rust with multiparty session types. In Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming(PPoPP \u201922). ACM, New York, NY, 246\u2013261. DOI: 10.1145\/3503221.3508404"},{"key":"e_1_3_2_16_1","first-page":"30 pages","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Das Ankush","year":"2018","unstructured":"Ankush Das, Jan Hoffmann, and Frank Pfenning. 2018. Parallel complexity analysis with temporal session types. Proceedings of the ACM on Programming Languages 2, ICFP, Article 91 (Jul. 2018), 30 pages. DOI: 10.1145\/3236786"},{"key":"e_1_3_2_17_1","unstructured":"FreeRTOS. 2003. FreeRTOS Kernel. Amazon Web Services. Retrieved from https:\/\/www.freertos.org\/"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Simon Gay and Malcolm Hole. 2005. Subtyping for session types in the pi calculus. Acta Informatica 42 2 (Nov. 2005) 191\u2013225. DOI: 10.1007\/s00236-005-0177-z","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_2_19_1","first-page":"23","volume-title":"Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES@ETAPS \u201920)EPTCS","volume":"314","author":"Gay Simon J.","year":"2020","unstructured":"Simon J. Gay, Peter Thiemann, and Vasco T. Vasconcelos. 2020. Duality of session types: The final cut. In Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES@ETAPS \u201920). Stephanie Balzer and Luca Padovani (Eds.), EPTCS, Vol. 314, 23\u201333. DOI: 10.4204\/EPTCS.314.3"},{"key":"e_1_3_2_20_1","first-page":"509","volume-title":"Concurrency Theory (CONCUR \u201993)","author":"Honda Kohei","year":"1993","unstructured":"Kohei Honda. 1993. Types for dyadic interaction. In Concurrency Theory (CONCUR \u201993). Eike Best (Ed.), Springer, Berlin, 509\u2013523."},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_3_2_22_1","first-page":"273","volume-title":"Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201908)","author":"Honda Kohei","year":"2008","unstructured":"Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201908). ACM, New York, NY, 273\u2013284. DOI: 10.1145\/1328438.1328472"},{"key":"e_1_3_2_23_1","first-page":"19:1","volume-title":"Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP \u201924)International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","author":"Hou Ping","year":"2024","unstructured":"Ping Hou, Nicolas Lagaillardie, and Nobuko Yoshida. 2024. Fearless asynchronous communications with timed multiparty session protocols. In Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP \u201924). LeibnizJonathan Aldrich and Guido Salvaneschi (Eds.), International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 19:1\u201319:30. DOI: 10.4230\/LIPIcs.ECOOP.2024.19"},{"key":"e_1_3_2_24_1","unstructured":"InfiniTime. 2020. InfiniTime. InfiniTime. Retrieved from https:\/\/github.com\/InfiniTimeOrg\/InfiniTime\/"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Grant Iraci Cheng-En Chuang Raymond Hu and Lukasz Ziarek. 2023. Rate based session types: Rust implementation. DOI: 10.1145\/3580415","DOI":"10.1145\/3580415"},{"key":"e_1_3_2_26_1","first-page":"29 pages","volume-title":"Proceedings of the ACM on Programming Languages","volume":"7","author":"Iraci Grant","year":"2023","unstructured":"Grant Iraci, Cheng-En Chuang, Raymond Hu, and Lukasz Ziarek. 2023. Validating IoT devices with rate-based session types. In Proceedings of the ACM on Programming Languages 7, OOPSLA2, Article 278 (Oct. 2023), 29 pages. DOI: 10.1145\/3622854"},{"key":"e_1_3_2_27_1","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/2808098.2808100","volume-title":"Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming(WGP \u201915)","author":"Jespersen Thomas Bracht Laumann","year":"2015","unstructured":"Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. 2015. Session types for rust. In Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming(WGP \u201915). ACM, New York, NY, USA, 13\u201322. DOI: 10.1145\/2808098.2808100"},{"key":"e_1_3_2_28_1","first-page":"4:1","volume-title":"Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP \u201922)Leibniz International Proceedings in Informatics (LIPIcs)","volume":"222","author":"Lagaillardie Nicolas","year":"2022","unstructured":"Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2022. Stay safe under panic: Affine rust programming with multiparty session types. In Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP \u201922). Karim Ali and Jan Vitek (Eds.), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 222, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 4:1\u20134:29. DOI: 10.4230\/LIPIcs.ECOOP.2022.4"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/JIOT.2017.2683200"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.141"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12652-016-0350-y"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12599-021-00689-w"},{"key":"e_1_3_2_34_1","volume-title":"Practical Session Types in Rust","author":"Munksgaard Philip","year":"2015","unstructured":"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_3_2_35_1","first-page":"311","volume-title":"Metatheory of Recursive Types.","author":"Pierce Benjamin C.","year":"2002","unstructured":"Benjamin C. Pierce. 2002. Types and programming languages. In Metatheory of Recursive Types. The MIT Press, 311\u2013312."},{"key":"e_1_3_2_36_1","unstructured":"Pine64. 2019. PineTime. Pine64. Retrieved from https:\/\/www.pine64.org\/pinetime\/"},{"key":"e_1_3_2_37_1","unstructured":"QNX. 2001. QNX Neutrino. QNX. Retrieved from https:\/\/www.qnx.com\/products\/intl\/neutrino_rtos\/"},{"key":"e_1_3_2_38_1","first-page":"30:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"3","author":"Scalas Alceste","year":"2019","unstructured":"Alceste Scalas and Nobuko Yoshida. 2019. Less is more: Multiparty session types revisited. Proceedings of the ACM on Programming Languages 3, POPL (2019), 30:1\u201330:29. DOI: 10.1145\/3290343"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2018.2873186"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.3390\/s19030477"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80382-2"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364568"},{"key":"e_1_3_2_43_1","unstructured":"Pete Warden. 2020. TinyML: Machine learning with tensorflow on Arduino and ultra-low Power Micro-controllers. O\u2019Reilly Media."},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00449-012-0848-4"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.13154\/tches.v2019.i3.66-85"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2008.04.002"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3754449","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T14:49:10Z","timestamp":1758120550000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3754449"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,17]]},"references-count":46,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3754449"],"URL":"https:\/\/doi.org\/10.1145\/3754449","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2025,9,17]]},"assertion":[{"value":"2024-09-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-21","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}