Page 81 - 《软件学报》2021年第7期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(7):19992015 [doi: 10.13328/j.cnki.jos.006272] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563


不确定环境下 hCPS 系统的形式化建模与动态验证

2
2
1
2
安冬冬 , 刘 静 , 陈小红 , 孙海英
1
(上海师范大学 信息与机电工程学院,上海 201418)
2
(华东师范大学 软件工程学院,上海 200062)
通讯作者: 刘静, E-mail: jliu@sei.ecnu.edu.cn

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

中文引用格式: 安冬冬,刘静,陈小红,孙海英.不确定环境下 hCPS 系统的形式化建模与动态验证.软件学报,2021,32(7):
19992015. http://www.jos.org.cn/1000-9825/6272.htm
英文引用格式: An DD, Liu J, Chen XH, Sun HY. Formal modeling and dynamic verification for human cyber physical systems
under uncertain environment. Ruan Jian Xue Bao/Journal of Software, 2021,32(7):19992015 (in Chinese). http://www.jos.org.
cn/1000-9825/6272.htm
Formal Modeling and Dynamic Verification for Human Cyber Physical Systems under
Uncertain Environment
2
2
1
AN Dong-Dong , LIU Jing , CHEN Xiao-Hong , SUN Hai-Ying 2
1 (The College of Information, Mechanical and Electrical Engineering, Shanghai Normal University, Shanghai 201418, China)
2 (Software Engineering Institute, East China Normal University, Shanghai 200062, China)
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

 基金项目: 国家重点研发计划(2019YFA0706404); 国家自然科学基金(61972150); 上海市知识服务平台(ZF1213); 上海市科
技计划(20ZR1416000); 上海市青年科技英才杨帆计划(21YF1432900)
Foundation item: 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)
本文由“面向非确定性的软件质量保障方法与技术”专题特约编辑陈俊洁副教授、汤恩义副教授、何啸副教授以及马晓星教授
推荐.
收稿时间: 2020-09-17; 修改时间: 2020-10-26; 采用时间: 2020-12-14; jos 在线出版时间: 2021-01-22