不确定环境下hCPS系统的形式化建模与动态验证
作者:
作者单位:

作者简介:

安冬冬(1990-),女,博士,CCF专业会员,主要研究领域为形式化建模与验证,统计模型检测,人机物融合系统,自动驾驶系统.
陈小红(1982-),女,博士,副教授,CCF专业会员,主要研究领域为需求工程,形式化方法,安全攸关系统.
刘静(1964-),女,博士,教授,博士生导师,CCF专业会员,主要研究领域为基于模型的高可信软件开发技术,形式化方法建模与验证.
孙海英(1976-),女,博士,讲师,CCF专业会员,主要研究领域为形式化建模,形式化验证,基于形式化的测试.

通讯作者:

刘静,E-mail:jliu@sei.ecnu.edu.cn

基金项目:

国家重点研发计划(2019YFA0706404);国家自然科学基金(61972150);上海市知识服务平台(ZF1213);上海市科技计划(20ZR1416000);上海市青年科技英才杨帆计划(21YF1432900)


Formal Modeling and Dynamic Verification for Human Cyber Physical Systems under Uncertain Environment
Author:
Affiliation:

Fund Project:

National Key R&D Program of China (2019YFA0706404); National Natural Science Foundation of China (61972150); Knowledge Service Platform of Shanghai (ZF1213); Shanghai Science and Technology Committee (20ZR1416000); Shanghai Sailing Program (21YF1432900)

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

    随着科技的进步,新型复杂系统,例如人机物融合系统(human cyber-physical systems,简称hCPS),已与人类社会生活越来越密不可分.软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.由于系统安全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决.因此,在不确定性环境下,构造智能、安全的人机物融合系统已成为软件行业所面临的不可回避的挑战.环境不确定性使得人机物融合系统软件无法准确感知其所处的运行环境.感知的不确定性将导致系统的误判,从而影响系统的安全性.环境不确定性使得系统设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约.而对于安全要求较高的系统,准确的形式化规约是保证系统安全的首要条件.为了应对规约的不确定性,提出时空数据驱动与模型驱动相结合的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模.根据安全软件的典型特征,采用动态验证的方式保证系统的安全,从而构建统一而安全的理论框架.为了展示方案的可行性,以自动驾驶车辆与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.

    Abstract:

    With the development of technology, new complex systems such as human cyber-physical systems (hCPS) have become indistinguishable from social life. The cyberspace where the software system located is increasingly integrated with the physical space of people's daily life. The uncertain factors such as the dynamic environment in the physical space, the explosive growth of the spatio-temporal data, as well as the unpredictable human behavior are all compromise the security of the system. As a result of the increasing security requirements, the scale and complexity of the system are also increasing. This situation leads to a series of problems that remain unresolved. Therefore, developing intelligent and safe human cyber-physical systems under uncertain environment is becoming the inevitable challenge for the software industry. It is difficult for the human cyber-physical systems to perceive the runtime environment accurately under uncertain surroundings. The uncertain perception will lead to the system's misinterpretation, thus affecting the security of the system. It is difficult for the system designers to construct formal specifications for the human cyber-physical systems under uncertain environment. For safety-critical systems, formal specifications are the prerequisites to ensure system security. To cope with the uncertainty of the specifications, a combination of data-driven and model-driven modeling methodology is proposed, that is, the machine learning-based algorithms are used to model the environment based on spatio-temporal data. An approach is introduced to integrate machine learning method and runtime verification technology as a unified framework to ensure the safety of the human cyber-physical systems. The proposed approach is illustrated by modeling and analyzing a scenario of the interaction of an autonomous vehicle and a human-driven motorbike.

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

安冬冬,刘静,陈小红,孙海英.不确定环境下hCPS系统的形式化建模与动态验证.软件学报,2021,32(7):1999-2015

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

京公网安备 11040202500063号