FCS 文章精要：华东师范大学朱惠彪教授团队——CaIT演算的证明系统。论文标题：A proof system of the CaIT calculus
期刊：Frontiers of Computer Science
作者：Ningning CHEN, Huibiao ZHU
发表时间：15 Apr 2024
DOI： 10.1007/s11704-022-2258-3
微信链接：点击此处阅读微信文章
导读
物联网（IoT）可以实现人、机、物随时随地互联互通。现有的研究大多集中在物联网的实际应用上，缺乏从形式化方法的角度对物联网系统进行建模和推理的研究。因此，CaIT（Calculus of the Internet of Things）演算被提出来，在物联网实际实施之前，对其进行建模和分析，从而可以有效提高物理网系统的开发效率，并确保系统的质量和可靠性。为了验证由CaIT演算描述的物联网系统的正确性，本文基于带有时间的霍尔逻辑，提出了CaIT演算的证明系统。此外，我们探索了单独的证明之间的协作关系，即它们相互协作验证这些证明中提到的通信行为的后置条件，其中广播通信是我们研究的重点。我们还证明了证明系统的正确。
