SmrCaIT演算的证明系统

《ACM Transactions on Embedded Computing Systems》：A Proof System for the SMrCaIT Calculus

本研究提出首个适用于物联网的进程代数SMrCaIT，用于全面描述系统安全、实时性和移动性特征。通过扩展Hoare逻辑构建证明系统，并采用合作测试验证消息传递正确性，在VANET和无人机系统中验证了方法的有效性，为构建可靠安全的物联网系统奠定理论基础。

　　

摘要

物联网（IoT）的快速发展推动了全球对相关应用和技术的强烈需求，尤其是在提高系统可靠性和安全性方面。通信安全、移动性和实时性是构建安全可靠物联网系统的三个关键特性。基于严格数学理论的形式化方法被广泛用于描述、分析、建模和验证软件和硬件系统，显著提升了它们的安全性和可靠性。然而，当前的研究主要集中在物联网的实际应用上，而将形式化方法应用于物联网系统的研究仍然较少。作为对此的回应，我们最近提出了SmrCaIT演算，这是目前唯一专为物联网设计的演算方法，能够全面描述物联网的安全性、实时性和移动性特征。通过应用SmrCaIT演算，我们可以在物联网系统实际部署之前对其进行建模和验证，从而为构建安全可靠的物联网系统提供坚实的理论基础。为了验证SmrCaIT程序的正确性，本文提出了一个基于扩展Hoare逻辑的SmrCaIT演算证明系统（该逻辑考虑了时间因素）。此外，我们还探讨了孤立证明之间的协作测试机制，以进一步确保物联网实体之间的消息能够正确传递。该证明系统的正确性也得到了验证。通过车辆自组织网络（VANET）和多无人机（Multi-UAV）案例，展示了我们证明系统在分析物联网场景中的实用性。