基于时间自动机的无信号交叉口车路协同系统建模与验证  

Modeling and Verification of Cooperative Vehicle Infrastructure System at Unsignalized Intersection Based on Time Automata

作　　者：刘伟[1] 肖七瑞 陈新海 饶畅 张宇 王博思 Liu Wei;Xiao Qirui;Chen Xinhai;Rao Chang;Zhang Yu;Wang Bosi(School of Traffic and Transportation,Chongqing Jiaotong University,Chongqing 400074,China;Chongqing Vehicle Test&Research Institute Co.,Ltd,Chongqing Engineering Research Center of Research and Testing for Automated Driving System and Intelligent Connected Vchicle,Chongqing 401122,China)

机构地区：[1]重庆交通大学交通运输学院,重庆400074 [2]重庆车辆检测研究院有限公司自动驾驶系统及智能网联汽车技术研发与测试应用重庆市工程研究中心,重庆401122

出　　处：《系统仿真学报》2024年第7期1682-1698,共17页Journal of System Simulation

基　　金：自动驾驶系统及智能网联汽车技术研发与测试应用重庆市工程研究中心课题(21AKC43);重庆市交通规划研究院交通运输工程研究生联合培养基金(JDLHPYJD2018004)。

摘　　要：车路协同系统(cooperative vehicle infrastructure system,CVIS)是提高交叉口车辆通行安全的重要解决方案之一。针对CVIS现有技术规范和标准未明确系统对象状态交互的动态时序及迁移过程,无法有效保障系统的通行控制逻辑安全问题,采用形式化语言对无信号交叉口车路协同系统功能逻辑进行描述,验证系统对象的状态交互和控制逻辑安全,提高无信号交叉口的车辆通行安全性。以单车无冲突、双车冲突和多车冲突场景分别进行仿真,明确状态交互和使能迁移路径;结合工具和需求规范语句进行系统安全属性验证,证明了控制逻辑的可靠性和安全性,为研发高安全架构的车路协同系统提供了可信依据。Cooperative vehicle infrastructure system(CVIS)is one of the advanced solutions to enhance intersection vehicle passage safety.Due to the lack of clear specifications and standards regarding the dynamic timing and transition processes of system object state interaction in existing CVIS technologies,ensuring the safety of passage control logic is challenging.This study utilizes formal language to describe the functional logic of CVIS in unsignalized intersections,verifying the safety of system object state interaction and control logic to improve vehicle passage safety at unsignalized intersections.Simulations are conducted for scenarios including single-vehicle non-conflict,dual-vehicle conflict,and multi-vehicle conflict to identify state interactions and enable transition paths.By integrating tools and requirement specification statements for system safety attribute verification,the reliability and safety of control logic are demonstrated,providing a credible basis for developing high-security architecture for CVIS.

关 键 词：城市交通 形式化语言 车路协同系统 时间自动机 控制逻辑 可信验证 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术] U495[自动化与计算机技术—计算机科学与技术]