详情

原文传递信控交叉口车路协同系统形式化建模与验证

论文题名：	信控交叉口车路协同系统形式化建模与验证
关键词：	道路交叉口;车路协同系统;形式化建模;统一建模语言;时间自动机;进口道
摘要：	车路协同系统作为城市交通拥堵问题的新一代解决方案，综合运用大数据、物联网和通信技术等保证路段车辆和行人安全有序的通过各个交通节点，时刻保证交通安全高效运行，其发展趋势是利用人工智能等技术实现交通系统中车辆高精度的全局最优控制。目前，车路协同技术得到了发展和试点应用，道路环境处于人工驾驶车辆与智能网联车辆混行的过渡阶段。信控交叉口是车路协同技术的一个重要应用场景，当信控交叉口出现智能网联车辆与人工驾驶车辆的混行交通状态时，传统人工驾驶车辆无法与路侧设备和其他车辆进行实时信息交互，其不确定的行为特征成为了系统协同安全运行的干扰因素。现有方法难以有效应对这种混合交通状态，为交叉口车路协同系统的安全决策控制带来了极大挑战，加剧了车辆碰撞、追尾等事故风险。　　形式化方法通过数学逻辑推导的方式进行系统模型构建、规约和验证，可减少对交互信息的依赖，显著提升系统的控制决策安全。针对上述问题，本文提出了一种基于形式化理论的车路协同交叉口系统安全保障方法，在研究交叉口车路协同系统混合车辆控制决策机理基础上，进行交叉口车路协同系统安全可靠性形式化映射与验证，为解决信控交叉口车路协同系统部分技术难点提供参考依据。主要内容如下：　　（1）提出信控交叉口车路协同系统混合车辆诱导机理　　首先构建信控交叉口进口道可量化的结构化场景，给出静态和动态信息相关定义。接着考虑信号灯剩余时长和人工驾驶员驾驶风格影响因素，提出以混合车辆的驾驶决策特征为基础的信控交叉口车路协同混合车辆诱导机理，分析系统中混合车辆控制工况逻辑和数学约束内容。　　（2）构建基于混合车辆诱导机理的车路协同信息交互过程模型　　首先基于智能网联车辆通信和控制相关规范标准框架，根据混合车辆诱导机理，提出基于混合车辆诱导机理的信控交叉口车路协同系统信息交互过程模型。采用统一建模语言进行系统建模，对自动驾驶车辆-路侧单元、人工驾驶车辆-路侧单元等信息交互过程进行精准刻画，明确了车路协同系统描述对象、功能状态参数、信息迁移时序和功能状态变化。　　（3）提出信控交叉口车路协同系统形式化验证方法　　首先基于时间自动机理论，提出信控交叉口车路协同系统的形式化建模方法，包括基于统一建模语言的信控交叉口车路协同系统时间自动机模型定义、动作及状态迁移表示方法等。在此基础上，给出时间自动机模型转换规则与系统安全属性的可满足性验证规则，并结合实际案例，分析了根据信控交叉口车路协同系统混合车辆的安全诱导和无冲突安全通行下的系统信息交互过程，验证了方法的有效性。
作者：	张宇
专业：	交通运输工程;交通运输规划与管理
导师：	刘伟
授予学位：	硕士
授予学位单位：	重庆交通大学
学位年度：	2023