近日，智慧教育学院（计算机科学与技术学院）祝义教授指导其硕士研究生陈小颖发表了一篇题为《面向CPS时空约束的资源建模及其安全性验证方法》的文章，刊登于国内计算机类顶级期刊《软件学报》(CCF A) 2022年第33卷第8期。

首先，文章介绍了信息物理融合系统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模型，直至满足所提出的安全需求。

最后，文章通过一个驾驶场景实例，验证了该方法的有效性。

作者简介：

陈小颖：江苏师范大学智慧教育学院（计算机科学与技术学院）硕士研究生；

祝义：江苏师范大学智慧教育学院（计算机科学与技术学院）教授、硕士生导师、副院长，江苏师范大学智能软件工程研究所所长，CCF高级会员，CCF形式化方法专委会委员，江苏省计算机学会理事，TSE、SPE、计算机学报等期刊审稿人。