随着汽车行业的蓬勃发展,交通事故数量也在大幅上升。自动驾驶技术应运而生,且日益兴起。但是其最重要的安全性一直是个具有挑战性的难题。因此自动驾驶技术大规模推广应用十分困难。辅助驾驶系统作为典型的信息物理融合系统,能够根据场景的变化辅助驾驶员进行安全驾驶,具有很大的应用前景。辅助驾驶系统的运行环境中存在着大量的不确定性,不仅包括车外驾驶场景的复杂多变,还包括车内驾驶员自身的不确定性。环境的不确定性,会导致系统的行为具有不确定性,是影响系统安全性的重要因素之一。形式化方法能够精确建模系统的行为,并支持使用模型检测技术分析,验证系统的行为正确性。如何使用形式化方法建模,分析辅助驾驶系统的不确定环境,是提高此类系统安全性所面临的重要挑战问题之一。因此本文从车内驾驶员因素和车外的周边场景因素着手,分别对车内外场景进行了建模及验证研究。本文的研究内容及成果主要有以下几点:1.针对车内的驾驶员的不确定性行为,本文提出了基于学习和模型检测的驾驶员行为分析方法。使用摄像头采集驾驶员数据,构建卷积神经网络(CNN)从图像中提取驾驶员特征数据,并使用朴素贝叶斯算法构建驾驶员状态预测模型。马尔科夫决策过程(MDP)模型可以很好地量化出驾驶员行为的不确定性及状态迁移概率。因此,根据生成状态预测模型,结合给定的驾驶员历史数据,可以构建出驾驶员的MDP模型。使用PRISM模型验证工具对基于MDP模型的驾驶员状态进行预测评估及量化分析。2.针对车外基于连续时间变化的场景,本文提出了基于随机混成自动机网络(NSHA)的场景建模及验证方法。使用条件蒙特卡洛密集占用追踪器(CMCDOT)框架,实现对环境的感知,有效获取周边车辆及行人的相关信息。根据辅助驾驶的车外场景的特征,例如周边车辆,道路状况等,抽取场景中重要对象,提出了场景特征树的表示方法。针对场景中连续变化的速度,位置等变量,NSHA可以对基于连续时间变化的系统进行有效地刻画描述。基于UPPAAL SMC验证工具,实现分析,评估场景的安全性。此外,我们给出了辅助驾驶算法,集成了基于NSHA建模及验证的场景安全性分析方法。3.为了证明本文所提方法的有效性,本文对三个典型的辅助驾驶场景案例进行了研究。用模拟驾驶软件CARLA,实现对三个典型场景的数据采集。并基于采集的数据,使用提出的方法构建出场景的NSHA模型,并用UPPAAL SMC实现了对各个场景的验证分析。验证分析的结果表明,本文所提出的验证分析方法能够有效量化预测自身车辆进入不安全状态的概率,评估当前及未来场景的安全程度。4.本文分别设计实现了MDP模型生成器与基于NSHA辅助驾驶场景的验证模型自动生成器软件。MDP模型生成器软件可用于自动化构建驾驶员行为的MDP模型,并将模型转换成对应的PRISM代码。验证模型自动生成器软件可以根据场景数据输入,自动化构建出UPPAAL SMC模型验证器可识别的NSHA模型。这两款工具软件为本文所提的理论方法提供了技术支撑,能够有效实现理论方法的工程应用。