典型文献
面向CPS时空约束的资源建模及其安全性验证方法
文献摘要：
信息物理融合系统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模型,直至满足所提出的安全需求;最后,通过一个驾驶场景实例,验证该方法的有效性.
文献关键词：
信息物理融合系统;进程代数;形式化验证;时空约束;资源安全性
中图分类号：
作者姓名：
陈小颖;祝义;赵宇;王金永
作者机构：
江苏师范大学 计算机科学与技术学院, 江苏 徐州 221116;高安全系统的软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学), 江苏 南京 210016
文献出处：
引用格式：
[1]陈小颖;祝义;赵宇;王金永-.面向CPS时空约束的资源建模及其安全性验证方法)[J].软件学报,2022(08):2815-2838
A类：
TCSP,顺序进程,BigMC,进程代数
B类：
CPS,时空约束,安全性验证,验证方法,信息物理融合系统,cyber,physical,system,环境感知,智能交互,物理空间,资源安全性,时空变化,安全性问题,timed,communicating,sequential,process,时空资源,DSR,duration,space,resource,性需求,安全需求,属性验证,模型转换,偶图,检验工具,反例,驾驶场景,形式化验证
AB值：
0.332924
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
