面向CPS时空约束的资源建模及其安全性验证方法
CSTR:
作者:
作者单位:

作者简介:

陈小颖(1997-),女,硕士,CCF学生会员,主要研究领域为软件工程,形式化方法,CPS系统;
赵宇(1997-),男,硕士,CCF学生会员,主要研究领域为软件工程,形式化方法,软件缺陷预测,机器学习;
祝义(1976-),男,博士,教授,CCF高级会员,主要研究领域为软件工程,形式化方法,CPS系统,智能软件开发;
王金永(1983-),男,博士生,CCF学生会员,主要研究领域为时空约束系统规约,协同无人驾驶安全性分析,形式化模型检测.

通讯作者:

祝义,E-mail:zhuy@jsnu.edu.cn

中图分类号:

TP311

基金项目:

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


Modeling and Safety Verification Method for CPS Time and Topology Constrained Resources
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    信息物理融合系统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模型,直至满足所提出的安全需求;最后,通过一个驾驶场景实例,验证该方法的有效性.

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

陈小颖,祝义,赵宇,王金永.面向CPS时空约束的资源建模及其安全性验证方法.软件学报,2022,33(8):2815-2838

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号