主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
安冬冬,刘静,陈小红,孙海英.不确定环境下人机物融合系统的形式化建模与动态验证.软件学报,2021,32(7):27-0
不确定环境下人机物融合系统的形式化建模与动态验证
Formal Modeling and Dynamic Verification for Human Cyber Physical Systems under Uncertain Environment
投稿时间:2020-09-17  修订日期:2020-10-26
DOI:10.13328/j.cnki.jos.006272
中文关键词:  人机物融合系统  机器学习  不确定性建模  形式化验证  统计模型检测
英文关键词:human cyber physical system  machine learning  uncertainty modeling  formal verification  statistical model checking
基金项目:国家重点研发计划项目(2019YFA0706404);国家自然科学基金(61972150);上海市知识服务平台(ZF1213);上海市科技计划项目(20ZR1416000)
作者单位E-mail
安冬冬 上海师范大学 信息与机电工程学院, 上海 200234  
刘静 华东师范大学 软件工程学院, 上海 200062 jliu@sei.ecnu.edu.cn 
陈小红 华东师范大学 软件工程学院, 上海 200062  
孙海英 华东师范大学 软件工程学院, 上海 200062  
摘要点击次数: 189
全文下载次数: 167
中文摘要:
      随着科技的进步,新型复杂系统例如人机物融合系统(Human Cyber-Physical Systems,HCPS)已经与人类社会生活越来越密不可分.软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.由于系统安全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决.因此,在不确定性环境下,构造智能、安全的人机物融合系统已经成为软件行业不可回避的挑战.环境不确定性使得人机物融合系统软件无法准确感知其所处的运行环境.感知的不确定性将导致系统的误判,从而影响系统的安全性.环境不确定性使得系统设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约.而对于安全要求较高的系统,准确的形式化规约是保证系统安全的首要条件.为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模.根据安全软件的典型特征,采用动态验证的方式保证系统的安全,从而构建统一安全的理论框架.为了展示方案的可行性,本文以自动驾驶车辆与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.
英文摘要:
      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 increaseing. This situation leads to a series of problems taat 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, we propose a combination of data-driven and model-driven modeling methodology, that is, we use the machine learning-based algorithms to model the environment based on spatio-temporal data. We introduce an approach to integrate machine learning method and runtime verification technology as a unified framework to ensure the safety of the human cyber-physical systems. We illustrate our approach by modeling and analyzing a scenario of the interaction of an autonomous vehicle and a human-driven motorbike.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利