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

doi:10.16182/j.issn1004731x.joss.23-0456

系统仿真学报 ›› 2024, Vol. 36 ›› Issue (7): 1682-1698.doi: 10.16182/j.issn1004731x.joss.23-0456

• 研究论文 • 上一篇

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

刘伟¹(), 肖七瑞¹(), 陈新海², 饶畅¹, 张宇¹, 王博思²

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

收稿日期:2023-04-18 修回日期:2023-05-31 出版日期:2024-07-15 发布日期:2024-07-12
通讯作者: 肖七瑞 E-mail:neway119@qq.com;m15215190891@163.com
第一作者简介:刘伟(1978-)，男，教授，博士，研究方向为交通工程、道路交通安全。E-mail：neway119@qq.com
基金资助:
自动驾驶系统及智能网联汽车技术研发与测试应用重庆市工程研究中心课题(21AKC43);重庆市交通规划研究院交通运输工程研究生联合培养基金(JDLHPYJD2018004)

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

Liu Wei¹(), Xiao Qirui¹(), Chen Xinhai², Rao Chang¹, Zhang Yu¹, Wang Bosi²

^1.School of Traffic and Transportation, Chongqing Jiaotong University, Chongqing 400074, China
^2.Chongqing Vehicle Test & Research Institute Co. , Ltd, Chongqing Engineering Research Center of Research;and Testing for Automated Driving System and Intelligent Connected Vehicle, Chongqing 401122, China

Received:2023-04-18 Revised:2023-05-31 Online:2024-07-15 Published:2024-07-12
Contact: Xiao Qirui E-mail:neway119@qq.com;m15215190891@163.com

摘要/Abstract

摘要：

车路协同系统(cooperative vehicle infrastructure system, CVIS)是提高交叉口车辆通行安全的重要解决方案之一。针对CVIS现有技术规范和标准未明确系统对象状态交互的动态时序及迁移过程，无法有效保障系统的通行控制逻辑安全问题，采用形式化语言对无信号交叉口车路协同系统功能逻辑进行描述，验证系统对象的状态交互和控制逻辑安全，提高无信号交叉口的车辆通行安全性。以单车无冲突、双车冲突和多车冲突场景分别进行仿真，明确状态交互和使能迁移路径；结合工具和需求规范语句进行系统安全属性验证，证明了控制逻辑的可靠性和安全性，为研发高安全架构的车路协同系统提供了可信依据。

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

Abstract:

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.

Key words: urban traffic, formal language, cooperative vehicle infrastructure system (CVIS), time automata, control logic, credible verification

中图分类号:

TP391.9

刘伟,肖七瑞,陈新海等 . 基于时间自动机的无信号交叉口车路协同系统建模与验证[J]. 系统仿真学报, 2024, 36(7): 1682-1698.

Liu Wei,Xiao Qirui,Chen Xinhai,et al . Modeling and Verification of Cooperative Vehicle Infrastructure System at Unsignalized Intersection Based on Time Automata[J]. Journal of System Simulation, 2024, 36(7): 1682-1698.

图/表 21

图1

图2

表1

表2

BNF语法

BNF语法	含义
$E < > e x p$	存在路径， $e x p$ 在该路径的某状态为真
$E [] e x p$	存在路径， $e x p$ 在该路径的所有状态为真
$A [] e x p$	对于所有路径， $e x p$ 在任一路径的所有状态为真
$A < > e x p$	对于所有路径， $e x p$ 在任一路径的某状态为真
$e x p → φ$	对于所有路径， $e x p$ 在任一路径的某状态为真， $φ$ 必然为真

表2

图3

图4

图5

图6

图7

图8

图9

表3

模型Car位置、通道说明

名称	定义	状态
位置集合L	normal	初始状态
	list	同时段接近区段车辆编队
	car_decelerate	请求减速状态
	car_stratrgy	减速策略状态
	pass	冲突下头车可通行状态
	no_pass	冲突下非头车可通行状态
	cross	通过冲突区段
初始位L₀	normal	初始状态
通道集合C	tri	车辆通信命令
	req	请求通行权命令
	list_first	冲突下队列头车
	not_first	冲突下队列非头车
	appr	允许车辆通行命令
	decelerate_stratrgy	通行减速策略
	leave	离开信号反馈
	after_leave	冲突头车通行后剩余车辆控制命令
时钟集合X	clock_time
状态时钟约束I	cross:clock_time<=4
状态转移路径E	${< n o r m a l, t r i, l i s t >, < l i s t, r e q, c l o c k_t i m e : = 0, c a r_d e c e l e r a t e >, < c a r_d e c e l e r a t e, l i s t_f i r s t, p a s s >, < c a r_d e c e l e r a t e, a p p r, c r o s s >, < c a r_d e c e l e r a t e, n o t_f i r s t, n o_p a s s >, < n o_p a s s, d e c e l e r a t e_s t r a t e g y, c a r_s t r a t e g y >, < c a r_s t r a t e g y, a f t e r, (d e c e l e r a t e = f a l s e, c o n_r e q = f a l s e, l i s t_n o_f i r s t = f a l s e, l i s t_f i r s t_a p p r = f a l s e, s t r a t e g y = f a l s e), l i s t >, < p a s s, a p p r, c r o s s >, < c r o s s, l e a v e, n o r m a l >};$

表3

图10

表4

模型rss位置、通道说明

名称	定义	状态
位置集合L	idel	初始状态
	con_vss	冲突判断
	no_vss	非冲突判断
初始位L₀	idel	初始状态
通道集合C	conflict	车辆冲突命令
	no_conflict	车辆非冲突命令
	req	请求通行权命令
	not_first	冲突下队列非头车
	list_first	冲突下队列头车
	decelerate_stratrgy	通行减速策略
	appr	允许车辆通行命令
	after_leave	冲突头车通行后剩余车辆控制命令
	leave	离开信号反馈
时钟集合X	—
状态时钟约束I	—
状态转移路径E	${< i d l e, c o n f l i c t, c o n = t r u e, c o n_v s s >, < i d l e, n o_c o n f l i c t, n o_c o n = t r u e, n o_v s s > < i d l e, a f t e r_l e a v e, (t r i g g e r = t r u e, a_c o u n t = 0, d_c o u n t + +, c_c o u n t = 0), i d l e >, < i d l e, l e a v e, (T_n u m b e r - -, n o_r_n u m b e r - -, n o_a_n u m b e r - -), i d l e >, < c o n_v s s, r e q, (c o n_r e q = t r u e, b_c o u n t + +), c o n_v s s >, < c o n_v s s, a p p r, l i s t_f i r s t_a p p r = t r u e, c o n_v s s >, < c o n_v s s, d e c e l e r a t e_s t r a t e g y, (s t r a t e g y = t r u e, c_c o u n t + +), c o n_v s s >, < c o n_v s s, l i s t_f i r s t, (c o n_l i s t_f i r s t = f a l s e, b_c o u n t - -), c o n_v s s >, < c o n_v s s, n o t_f i r s t, (l i s t_n o_f i r s t = t r u e, b_c o u n t - -), c o n_v s s >, < c o n_v s s, l e a v e, (c o n_l i s t_f i r s t = t r u e, l i s t_f i r s t_l e a v e = t r u e, T_n u m b e r - -, c o n = f a l s e), i d l e >, < n o_v s s, r e q, n o_r_n u m b e r + +, n o_v s s >, < n o_v s s, a p p r, n o_a_n u m b e r + +, n o_v s s >, < n o_v s s, l e a v e, (T_n u m b e r - -, n o_r_n u m b e r - -, n o_a_n u m b e r - -, a_c o u n t = 0, d_c o u n t = 0, t r i g g e r = t r u e, n o_c o n = f a l s e), i d l e >}$

表4

图11

表5

模型Envir位置、通道说明

名称	定义	状态
位置集合L	rem	初始状态
	begin	车辆通信阶段判断
	next	剩余车辆再判断
初始位L₀	rem	初始状态
通道集合C	tri	请求通行权命令
	conflict	车辆冲突命令
	no_conflict	车辆非冲突命令
时钟集合X	—
状态时钟约束I	—
状态转移路径E	${< r e m, t r i, (T_n u m b e r + +, a_c o u n t + +), b e g i n >, < r e m, (l i s t_f i r s t_l e a v e = f a l s e, d_c o u n t = 0), n e x t >, < b e g i n, t r i, (T_n u m b e r + +, a_c o u n t + +), b e g i n >, < b e g i n, c o n f l i c t, t r i g g e r = f a l s e, r e m >, < b e g i n, n o_c o n f l i c t, r e m >, < n e x t, n o_c o n f l i c t, r e m >, < n e x t, c o n f l i c t, t r i g g e r = f a l s e, r e m >}$

表5

图12

图13

图14

表6

图15

参考文献 27

1	Chen Xiaolong, Hu Manjiang, Xu Biao, et al. Improved Reservation-based Method with Controllable Gap Strategy for Vehicle Coordination at Non-signalized Intersections[J]. Physica A: Statistical Mechanics and Its Applications, 2022, 604: 127953.
2	Dey K C, Rayamajhi A, Chowdhury M, et al. Vehicle-to-vehicle (V2V) and Vehicle-to-infrastructure (V2I) Communication in a Heterogeneous Wireless Network-performance Evaluation[J]. Transportation Research Part C: Emerging Technologies, 2016, 68: 168-184.
3	Grembek O, Kurzhanskiy A, Medury A, et al. Making Intersections Safer with I2V Communication[J]. Transportation Research Part C: Emerging Technologies, 2019, 102: 396-410.
4	Banks V A, Plant K L, Stanton N A. Driver Error or Designer Error: Using the Perceptual Cycle Model to Explore the Circumstances Surrounding the Fatal Tesla Crash on 7th May 2016[J]. Safety Science, 2018, 108: 278-285.
5	易振国. 车路协同实验测试系统及安全控制技术研究[D]. 长春: 吉林大学, 2011.
	Yi Zhenguo. Vehicle Infrastructure Integration Experimental Testing System and Safety Control Technology[D]. Changchun: Jilin University, 2011.
6	上官伟, 李鑫, 柴琳果, 等. 车路协同环境下混合交通群体智能仿真与测试研究综述[J]. 交通运输工程学报, 2022, 22(3): 19-40.
	Shangguan Wei, Li Xin, Chai Linguo, et al. Research Review on Simulation and Test of Mixed Traffic Swarm in Vehicle-infrastructure Cooperative Environment[J]. Journal of Traffic and Transportation Engineering, 2022, 22(3): 19-40.
7	Elsayed G F, Shankar S, Cheung B, et al. Adversarial Examples that Fool Both Computer Vision and Time-limited Humans[C]//Proceedings of the 32nd International Conference on Neural Information Processing Systems. Red Hook, NY, USA: Curran Associates Inc., 2018: 3914-3924.
8	Gleirscher M, Foster S, Woodcock J. New Opportunities for Integrated Formal Methods[J]. ACM Computing Surveys, 2020, 52(6): 117.
9	Russo Aryldo G, Ladenberger Lukas. A Formal Approach to Safety Verification of Railway Signaling Systems[C]//2012 Proceedings Annual Reliability and Maintainability Symposium. Piscataway, NJ, USA: IEEE, 2012: 1-4.
10	Steve Jeffrey Tueno Fotso, Frappier Marc, Laleau Régine, et al. Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach[J]. International Journal on Software Tools for Technology Transfer, 2020, 22(3): 349-363.
11	Muhammed Ali O Z, Ozgur Turay Kaymakci. An Automatic Formal Model Generation and Verification Method for Railway Interlocking Systems[J]. Gazi University Journal of Science, 2017, 30(2): 133-147.
12	Xu Bingqing, Li Qin, Guo Tong, et al. A Scenario-based Approach for Formal Modelling and Verification of Safety Properties in Automated Driving[J]. IEEE Access, 2019, 7: 140566-140587.
13	王淑灵, 詹博华, 盛欢欢, 等. 可信系统性质的分类和形式化研究综述[J]. 软件学报, 2022, 33(7): 2367-2410.
	Wang Shuling, Zhan Bohua, Sheng Huanhuan, et al. Survey on Requirements Classification and Formalization of Trustworthy Systems[J]. Journal of Software, 2022, 33(7): 2367-2410.
14	王鲲. 基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证[J]. 中国铁道科学, 2018, 39(3): 101-109.
	Wang Kun. Formal Modeling and Verification of CBTC Computer Interlocking System Based on Communication Sequential Process and B Method[J]. China Railway Science, 2018, 39(3): 101-109.
15	赵梦瑶, 陈小红, 孙海英, 等. 轨道交通联锁领域特定语言的形式化[J]. 软件学报, 2020, 31(6): 1638-1653.
	Zhao Mengyao, Chen Xiaohong, Sun Haiying, et al. Formalizing Railway Interlocking Domain Specific Language[J]. Journal of Software, 2020, 31(6): 1638-1653.
16	Lefebvre Dimitri, Hadjicostis Christoforos N. Diagnosability of Fault Patterns with Labeled Stochastic Petri nets[J]. Information Sciences, 2022, 593: 341-363.
17	中华人民共和国工业和信息化部. 基于车路协同的高等级自动驾驶数据交互内容: [S].
	Ministry of Industry and Information Technology of the People's Republic of China. Data Exchange Standard for High Level Automated Driving Vehicle Based on Cooperative Intelligent Transportation System: [S].
18	崔晓丹. 基于车路协同的区域化无信号交叉口控制方法研究[D]. 北京: 北京交通大学, 2017.
	Cui Xiaodan. Research on Regional Unsignalized-intersection Control Method Based on Cooperative Vehicle Infrastructure System[D]. Beijing: Beijing Jiaotong University, 2017.
19	孙伟, 张梦雅, 马成元, 等. 新型混合交通交叉口信号与车辆轨迹协同控制方法[J]. 交通运输系统工程与信息, 2023, 23(1): 97-105.
	Sun Wei, Zhang Mengya, Ma Chengyuan, et al. Coordination of Signal and Vehicle Trajectory at Intersections for Mixed Traffic Flow[J]. Journal of Transportation Systems Engineering and Information Technology, 2023, 23(1): 97-105.
20	Qu Dayi, Zhao Zixu, Song Hui, et al. Design of Vehicle-road Cooperative Assistant Decision System for Active Safety at Intersections[J]. Journal of Transportation Engineering, Part A: Systems, 2022, 148(5): 04022022.
21	张毅, 姚丹亚, 李力, 等. 智能车路协同系统关键技术与应用[J]. 交通运输系统工程与信息, 2021, 21(5): 40-51.
	Zhang Yi, Yao Danya, Li Li, et al. Technologies and Applications for Intelligent Vehicle-infrastructure Cooperation Systems[J]. Journal of Transportation Systems Engineering and Information Technology, 2021, 21(5): 40-51.
22	Wang Yang, Ning Wei, Zhang Shengyu, et al. Architecture and Key Terminal Technologies of 5G-based Internet of Vehicles[J]. Computers and Electrical Engineering, 2021, 95: 107430.
23	Rumbaugh J, Jacobson I, Booch G. The Unified Modeling Language Reference Manual[M]. 2nd ed. Boston: Addison-Wesley, 2005.
24	韩德帅, 杨启亮, 邢建春. 一种软件自适应UML建模及其形式化验证方法[J]. 软件学报, 2015, 26(4): 730-746.
	Han Deshuai, Yang Qiliang, Xing Jianchun. UML-based Modeling and Formal Verification for Software Self-adaptation[J]. Journal of Software, 2015, 26(4): 730-746.
25	Bengtsson Johan, Kim Larsen, Larsson Fredrik, et al. UPPAAL-a tool Suite for Automatic Verification of Real-time Systems[C]//Hybrid Systems III. Berlin, Heidelberg: Springer Berlin Heidelberg, 1996: 232-243.
26	Alur R, Dill D L. A Theory of Timed Automata[J]. Theoretical Computer Science, 1994, 126(2): 183-235.
27	Ortmeier Frank, Reif Wolfgang, Schellhorn Gerhard. Formal Safety Analysis of a Radio-based Railroad Crossing Using Deductive Cause-consequence Analysis (DCCA)[C]//Dependable Computing-EDCC 5. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005: 210-224.

主要构成	主要功能
系统编辑器	创建和编辑实时系统模型
模拟器	模拟系统模型状态迁移情况等
验证器	验证模型的功能属性

序列	性质
P1	A[]not deadlock
P2	A[]((deadlock imply(Carl.normal and Car2.normal and Car3.normal and rss.idle and Envir.rem)))
P3	E>Car1.cross and Car2.car_stratrgy and Car3.car_stratrgy
P4	E<>Car1.cross or Car2.cross or Car3.cross
P5	A>Car1.cross+Car2.cross+Car3.cross<=1
P6	A[]((Car1.cross imply(Car1.clock_time<=4)))

[1]	朱依婷, 闫云, 何兆成. 公交与社会车辆混合的中观交通建模与仿真[J]. 系统仿真学报, 2022, 34(09): 2019-2027.
[2]	张振海, 姚婕. 基于时间自动机的C3+ATO系统场景建模与验证[J]. 系统仿真学报, 2021, 33(4): 951-961.
[3]	李卓君, 陈星光. 基于个体出行决策分析的交通流演化模型与仿真[J]. 系统仿真学报, 2015, 27(4): 866-874.

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

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

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 21

参考文献 27

相关文章 3

编辑推荐

Metrics

本文评价