随着科技的进步,新型复杂系统例如人机物融合系统(Human Cyber-Physical Systems,HCPS)已经与人类社会生活越来越密不可分。软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合。物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全。由于系统安全需求的增长,系统的规模和复杂度?随之增加,所带来的的一系列问题亟待解决。因此,在不确定环境下,构造智能、安全的人机物融合系统的建模与验证方法以及工具链平台的开发已经成为软件行业不可回避的挑战。环境不确定性使得人机物融合系统软件无法准确感知其所处的运行环境。感知的不确定性将导致系统的误判,从而影响系统的安全性。环境不确定性使得系统设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约。而对于安全要求较高的系统,准确的形式化规约是保证系统安全的首要条件。为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合的建模方式,即通过使用机器学习算法,基于环境中时空数据,而非基于形式化规约,对环境进行建模。根据安全软件的典型特征,设计具有层次化特征的参数化建模语言,采用动态验证的方式保证系统的安全,从而构建统一安全的理论框架。本文以构建安全智能的人机物融合系统的形式化建模与验证的理论框架及应用作为主要的研究目标。主要贡献体现在:·针对系统所处的物理环境的不确定性,应用机器学习技术,以环境中的时空数据为驱动,提出了不确定环境下的感知模型。包括基于朴素贝叶斯的人类行为分类模型和基于LSTM循环神经网络的环境风险预测模型。·定义了具有层次化特征的参数化建模语言stohChart(p),给出了相应语法和语义的形式化定义。提出了将模型转换为随机混成自动机(Stochastic Hybrid Automaton,SHA)的映射算法。·提出针对不确定性模型的动态验证方法,通过验证工具UPPAAL-SMC实现对模型的动态验证,从而定量评估不确定性环境以及人的行为对系统安全性的影响。为了展示方案的可行性,本文以自动驾驶车辆与人类驾驶车辆的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用。