A Proof System for the SMrCaIT Calculus

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 cooperation test 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.