论文标题：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演算的证明系统。此外，我们探索了单独的证明之间的协作关系，即它们相互协作验证这些证明中提到的通信行为的后置条件，其中广播通信是我们研究的重点。我们还证明了证明系统的正确性，并给出了一个简单的“智能家居”案例来说明这个证明系统的可用性。

文章信息

相关内容推荐：

文章精要 | 最小和最大度点删除问题在若干特殊图上的参数复杂性 2023 17(4)：174405

文章精要 | 一种面向无线传感器网络中Set k-Cover问题的混合阶局部搜索算法 2023 17(3)：173402

文章精要 | 东北师范大学付治国教授团队：局部全息变换：可解性与困难性 2023 17(2)：172401

随机RB模型的超解研究 2022 16(6)：166406

一种用于基于定理证明同步模型验证的动态逻辑 2022 16(4)：1644057

赋范下推自动机互模拟等价的参数复杂性 2022 16(4)：164405

随机正则(s,c,k)-SAT问题的可满足临界 2022 16(3)：163408

图mCn的全友好指数集 2022 16(3)：163403

正则区间图边删除问题的一个改进算法 2022 16(2)：162401

再论近似部分优化问题的线性规划舍入加贪心方法 2022 16(1)：161402

Frontiers of Computer Science

Frontiers of Computer Science （FCS）是由教育部主管、高等教育出版社和北京航空航天大学共同主办、SpringerNature 公司海外发行的英文学术期刊。本刊于 2007 年创刊，双月刊，全球发行。主要刊登计算机科学领域具有创新性的综述论文、研究论文等。本刊主编为周志华教授，共同主编为熊璋教授。编委会及青年 AE 团队由国内外知名学者及优秀青年学者组成。本刊被 SCI、Ei、DBLP、INSPEC、SCOPUS 和中国科学引文数据库（CSCD）核心库等收录，为 CCF 推荐期刊；两次入选“中国科技期刊国际影响力提升计划”；入选“第4届中国国际化精品科技期刊”；入选“中国科技期刊卓越行动计划项目”。

《前沿》系列英文学术期刊

由教育部主管、高等教育出版社主办的《前沿》（Frontiers）系列英文学术期刊，于2006年正式创刊，以网络版和印刷版向全球发行。系列期刊包括基础科学、 、工程技术和人文社会科学四个主题，是我国覆盖学科最广泛的英文学术期刊群，其中12种被SCI收录，其他也被A&HCI、Ei、MEDLINE或相应学科国际权威检索系统收录，具有一定的国际学术影响力。系列期刊采用在线优先出版方式，保证文章以最快速度发表。

中国学术前沿期刊网

http://journal.hep.com.cn