软件学报

作者：刘靖宇，李晅松，陈芝菲，叶海波，宋巍

单位：刘靖宇，南京理工大学 计算机科学与工程学院, 江苏 南京 21009411,李晅松，南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,陈芝菲，南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,叶海波，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110604,宋巍，南京理工大学 计算机科学与工程学院, 江苏 南京 21009405

关键词：模型检测;物联网;形式化验证;建模语言

基金：国家自然科学基金(61702263, 61761136003); CCF-华为创新研究计划(CCF-HuaweiFM2021004)

物联网设备的使用范围正在不断扩张. 模型检测是提升这类设备可靠性和安全性的有效手段, 但常用的模型检测方法不能很好地刻画这类设备常见的跨空间移动和通信行为. 为此, 提出一种面向物联网设备移动与通信行为的建模及验证方法, 以实现对这类设备时空相关性质的验证. 通过将推拉动作和全局通信机制融入ambient calculus, 提出全局通信移动环境演算(ACGC)并给出了ACGC对ambient logic的模型检测算法; 在此基础上, 提出描述物联网设备移动和通信行为的移动通信建模语言(MLMC), 并给出将MLMC描述转换为ACGC模型的方法; 进一步地, 实现模型检测工具ACGCCk以验证物联网设备的性质是否得到满足, 并通过一些优化加快检测速度; 最后, 通过案例研究和实验分析阐明所提方法的有效性.

来源：2024年第11期

《软件学报》期刊编辑部

查看软件学报杂志2024年第11期