{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T22:59:19Z","timestamp":1783465159527,"version":"3.55.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"name":"National Key Research and Development Program of China","award":["2022YFB3305102"],"award-info":[{"award-number":["2022YFB3305102"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62032024 and 62402319"],"award-info":[{"award-number":["62032024 and 62402319"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cDigital Silk Road\u201d Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]},{"name":"Shanghai Trusted Industry Internet Software Collaborative Innovation Center"},{"name":"National Trusted Embedded Software Engineering Technology Research Center"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    The rapid development of the Internet of Things (IoT) spurs strong global demand for related applications and technologies, especially in enhancing system reliability and security. Communication security, mobility, and real-time are the three vital features for constructing secure and reliable IoT systems. Formal methods, based on rigorous mathematical theory, are widely used to describe, analyze, model, and verify software and hardware systems, significantly improving their security and reliability. However, the current research mainly focuses on the practical applications of IoT, and there are still few studies on applying formal methods to IoT systems. As a response, our recent work has proposed the SMrCaIT calculus, which is the only process calculus currently designed for IoT that can comprehensively describe the security, real-time, and mobile features of IoT. Applying the SMrCaIT calculus enables us to model and verify IoT systems before their actual implementation, thereby providing a solid theoretical foundation for building secure and reliable IoT systems. To verify the correctness of the SMrCaIT programs, this article presents a proof system for SMrCaIT calculus, based on the extended Hoare Logic considering time. Additionally, we explore the\n                    <jats:italic toggle=\"yes\">cooperation test<\/jats:italic>\n                    between isolated proofs to further ensure that messages are delivered correctly between IoT entities. The soundness of the proof system is also confirmed. A Vehicle Ad Hoc Network case and a Multi-Unmanned Aerial Vehicle case demonstrate the usability of our proof system in analyzing IoT scenarios.\n                  <\/jats:p>","DOI":"10.1145\/3701729","type":"journal-article","created":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T05:40:38Z","timestamp":1729748438000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Proof System for the SMrCaIT Calculus"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4795-9046","authenticated-orcid":false,"given":"Ningning","family":"Chen","sequence":"first","affiliation":[{"name":"University of Shanghai for Science and Technology","place":["Shanghai, China"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"East China Normal University","place":["Shanghai, China"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,3,5]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.phycom.2014.01.006"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40561-7_3"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Chiara Bodei Pierpaolo Degano Gian Luigi Ferrari and Letterio Galletta. 2016. Where do your IoT ingredients come from? In Coordination Models and Languages. Lecture Notes in Computer Science Vol. 9686.Springer 35\u201350.","DOI":"10.1007\/978-3-319-39519-7_3"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1002\/wcm.72"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1002\/smr.2595"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-022-2258-3"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.05.002"},{"key":"e_1_3_1_15_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.4108\/eai.10-6-2021.170230"},{"key":"e_1_3_1_17_2","doi-asserted-by":"crossref","unstructured":"Jens Chr. Godskesen. 2007. A calculus for mobile ad hoc networks. In Coordination Models and Languages. Lecture Notes in Computer Science Vol. 4467. Springer 132\u2013150.","DOI":"10.1007\/978-3-540-72794-1_8"},{"key":"e_1_3_1_18_2","doi-asserted-by":"crossref","unstructured":"Jens Chr. Godskesen. 2008. A calculus for mobile ad-hoc networks with static location binding. Electrical Notes in Theoretical Computer Science 242 1 (2009) 161\u2013183.","DOI":"10.1016\/j.entcs.2009.06.018"},{"key":"e_1_3_1_19_2","doi-asserted-by":"crossref","unstructured":"Jens Chr. Godskesen and Sebastian Nanz. 2009. Mobility models and behavioural equivalence for wireless networks. In Coordination Models and Languages. Lecture Notes in Computer Science Vol. 5521. Springer 106\u2013122.","DOI":"10.1007\/978-3-642-02053-7_6"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3103725"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Jifeng He and Qin Li. 2017. A hybrid relational modelling language. In Concurrency Security and Puzzles. Lecture Notes in Computer Science Vol. 10160. Springer 124\u2013143.","DOI":"10.1007\/978-3-319-51046-0_7"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_3_1_25_2","volume-title":"Unifying Theories of Programming","author":"Hoare C. A. R.","year":"1998","unstructured":"C. A. R. Hoare and Jifeng He. 1998. Unifying Theories of Programming. Vol. 14. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213604"},{"key":"e_1_3_1_27_2","unstructured":"G\u00e9rard Huet Gilles Kahn and Christine Paulin-Mohring. 1997. The Coq Proof Assistant: A Tutorial\u2014Version 7.2. Research Report RT-0256. INRIA."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480615"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.01.001"},{"key":"e_1_3_1_30_2","volume-title":"Consistent Formal Theories of the Semantics of Programming Languages","author":"Lauer Peter E.","year":"1971","unstructured":"Peter E. Lauer. 1971. Consistent Formal Theories of the Semantics of Programming Languages. Ph.D. Dissertation. Queen\u2019s University Belfast, UK."},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2576235"},{"key":"e_1_3_1_32_2","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","year":"2005","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"e_1_3_1_36_2","first-page":"279","volume-title":"Proceedings of the Working Conference on Formal Description of Programming Concepts","author":"Owicki Susan S.","year":"1977","unstructured":"Susan S. Owicki. 1977. Verifying concurrent programs with shared data classes. In Proceedings of the Working Conference on Formal Description of Programming Concepts. 279\u2013300."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90158-5"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"David San\u00e1n Yongwang Zhao Zhe Hou Fuyuan Zhang Alwen Tiu and Yang Liu. 2017. CSimpl: A Rely-Guarantee-based framework for verifying concurrent programs. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science Vol. 10205. Springer 481\u2013498.","DOI":"10.1007\/978-3-662-54577-5_28"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3436808"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.07.008"},{"key":"e_1_3_1_43_2","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"Stoy Joseph E.","year":"1977","unstructured":"Joseph E. Stoy. 1977. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press."},{"key":"e_1_3_1_44_2","volume-title":"Concurrent Verification for Sequential Programs","author":"Wickerson John","year":"2013","unstructured":"John Wickerson. 2013. Concurrent Verification for Sequential Programs. Ph.D. Dissertation. University of Cambridge, UK."},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"},{"key":"e_1_3_1_46_2","unstructured":"Bohua Zhan. 2022. User interface design in the HolPy theorem prover (invited talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022) June Andronick and Leonardo de Moura (Eds.). Leibniz International Proceedings in Informatics Vol. 237. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany Article 2 1 page."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3701729","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T09:27:14Z","timestamp":1773566834000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3701729"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,5]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3701729"],"URL":"https:\/\/doi.org\/10.1145\/3701729","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,5]]},"assertion":[{"value":"2024-01-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}