A proof system of the CaIT calculus  

作　　者：Ningning CHEN Huibiao ZHU 

机构地区：[1]Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China

出　　处：《Frontiers of Computer Science》2024年第2期123-137,共15页中国计算机科学前沿（英文版）

基　　金：supported by the National Key Research and Development Program of China (No.2022YFB3305102);the National Natural Science Foundation of China (Grant Nos.62032024,61872145);the"Digital Silk Road"Shanghai International Joint Lab of Trustworthy Intelligent Software (No.22510750100);Shanghai Trusted Industry Internet Software Collaborative Innovation Center,and the Dean's Fund of Shanghai Key Laboratory of Trustworthy Computing (East China Normal University).

摘　　要：The Internet of Things(IoT)can realize the interconnection of people,machines,and things anytime,anywhere.Most of the existing research mainly focuses on the practical applications of IoT,and there is a lack of research on modeling and reasoning about IoT systems from the perspective of formal methods.Thus,the Calculus of the Internet of Things(CaIT)has been proposed to specify and analyze IoT systems before the actual implementation,which can effectively improve development efficiency,and enhance system quality and reliability.To verify the correctness of IoT systems described by CaIT,this paper presents a proof system for CaIT,in which specifications and verifications are based on the extended Hoare Logic with time.Furthermore,we explore the cooperation between isolated proofs to validate the postconditions of the communication actions occurring in these proofs,with a particular focus on broadcast communication.We also demonstrate the soundness of our proof system.A simple“smart home”is given to illustrate the availability of our proof system.

关 键 词：Internet of Things(loT) Calculus of the Internet of Things(CalT) extended hoare logic COOPERATION smart home 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]