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

Modeling and Safety Verification Method for CPS Time and Topology Constrained Resources

作　　者：陈小颖 祝义[1,2] 赵宇 王金永[2] CHEN Xiao-Ying;ZHU Yi;ZHAO Yu;WANG Jin-Yong(School of Computer Science and Technology,Jiangsu Normal University,Xuzhou 221116,China;Key Laboratory for Safety-Critical Software Development and Verification(Nanjing University of Aeronautics and Astronautics),Ministry of Industry and Information Technology,Nanjing 210016,China)

机构地区：[1]江苏师范大学计算机科学与技术学院,江苏徐州221116 [2]高安全系统的软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学),江苏南京210016

出　　处：《软件学报》2022年第8期2815-2838,共24页Journal of Software

基　　金：国家自然科学基金(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的时间属性验证算法对时间安全需求进行验证;再次,将满足时间安全需求的模型转换为偶图与偶图反应,并输入到偶图检验工具Big MC中,验证其物理拓扑安全需求,对没有通过验证的反例,修改DSR-TCSP模型,直至满足所提出的安全需求;最后,通过一个驾驶场景实例,验证该方法的有效性.CPS(cyber physical system)combines physics and computation on the basis of environment perception and can realize intelligent interaction with the environment.However,the constant change of cyber physical space poses some challenges to the safety of CPS resources.Therefore,how to study this kind of CPS resource safety problems caused by topology and time changes becomes the key.This study proposes a CPS-oriented resource modeling and safety verification method to solve this problem.Firstly,on the basis of TCSP(timed communicating sequential process),resource vector is extended and DSR-TCSP(duration-space resource TCSP)is proposed,enable it to describe resources in the CPS topology.Secondly,the time safety requirements are obtained from the resource safety requirements of space and time constraints,and verified by the time verification algorithm of DSR-TCSP.Thirdly,the model meeting the time safety requirements is converted to the reaction of bigraphs and bigraphs reactive system,and the model is input into the bigraphs testing tool BigMC to verify its physical topology safety requirements.For the counter examples that do not pass the verification,the DSR-TCSP model is modified until the proposed safety requirements are met.Finally,a driving scenario is given to verify the effectiveness of the proposed method.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]