软件学报

作者：陈小颖，祝义，赵宇，王金永

单位：陈小颖，江苏师范大学 计算机科学与技术学院, 江苏 徐州 22111611,祝义，江苏师范大学 计算机科学与技术学院, 江苏 徐州 221116;高安全系统的软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学), 江苏 南京 21001602,赵宇，江苏师范大学 计算机科学与技术学院, 江苏 徐州 22111603,王金永，高安全系统的软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学), 江苏 南京 21001604

关键词：信息物理融合系统;进程代数;形式化验证;时空约束;资源安全性

基金：国家自然科学基金(62077029);南京航空航天大学基本科研业务费科研基地创新基金(NJ2020022);未来网络科研基金(FNSRFP-2021-YB-32);徐州市应用基础研究计划(KC19004);江苏省研究生科研创新计划(KYCX20_2380);江苏省研究生科研创新计划(KYCX20_2384)

信息物理融合系统CPS (cyber physical system)是在环境感知的基础上,集合物理与计算的系统,可以实现与环境的智能交互.CPS信息物理空间的不断变化,对CPS资源安全性造成一定的挑战.因此,如何研究这一类由时空变化而导致的CPS资源安全性问题成为关键.针对该问题,提出了面向CPS时空约束的资源建模及其安全性验证方法.首先,在TCSP (timed communicating sequential process)的基础上扩展资源向量,提出了时空资源通信顺序进程DSR-TCSP (duration-space resource TCSP),使其能够描述CPS拓扑环境下的资源;其次,从时空约束的资源安全性需求中获取时间安全需求,通过DSR-TCSP的时间属性验证算法对时间安全需求进行验证;再次,将满足时间安全需求的模型转换为偶图与偶图反应,并输入到偶图检验工具BigMC中,验证其物理拓扑安全需求,对没有通过验证的反例,修改DSR-TCSP模型,直至满足所提出的安全需求;最后,通过一个驾驶场景实例,验证该方法的有效性.

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期