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

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

车路协同系统(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.