首页|A proof system of the CaIT calculus

A proof system of the CaIT calculus

扫码查看
原文链接
  • NETL
  • NSTL
  • 万方数据
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(IoT)Calculus of the Internet of Things(CaIT)extended hoare logiccooperationsmart home

Ningning CHEN、Huibiao ZHU

展开 >

Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China

国家重点研发计划国家自然科学基金国家自然科学基金the"Digital Silk Road"Shanghai International Joint Lab of Trustworthy Intelligent SoftwareShanghai Trusted Industry Internet Software Collaborative Innovation CenterDean's Fund of Shanghai Key Laboratory of Trustworthy Computing(East China Normal University)

2022YFB3305102620320246187214522510750100

2024

10.1007/s11704-022-2258-3

计算机科学前沿
高等教育出版社

计算机科学前沿

CSTPCDEI
影响因子：0.303
ISSN：2095-2228
年,卷(期)：2024.18(2)
  • 29