面向CPS时空约束的资源建模及其安全性验证方法

作者：陈小颖; 祝义^*; 赵宇; 王金永

来源：软件学报, 2022, 33(08): 2815-2838.

DOI：10.13328/j.cnki.jos.006600

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

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

• 单位
  南京航空航天大学; 工业和信息化部; 江苏师范大学