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

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

随着科技的进步,新型复杂系统,例如人机物融合系统(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 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.