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

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

Abstract

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

CLC Number:

TP391.9

Liu Wei, Xiao Qirui, Chen Xinhai, Rao Chang, Zhang Yu, Wang Bosi. 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.

Figures/Tables 21

Fig. 1

Fig. 2

Table 1

Table 2

BNF grammar

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$ 在任一路径的某状态为真， $φ$ 必然为真

Table 2

Fig. 3

Fig. 4

Fig. 5

Fig. 6

Fig. 7

Fig. 8

Fig. 9

Table 3

Model car location and channel description

名称	定义	状态
位置集合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 >};$

Table 3

Fig. 10

Table 4

Model RSS location and channel description

名称	定义	状态
位置集合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 >}$

Table 4

Fig. 11

Table 5

Model Envir location and channel description

名称	定义	状态
位置集合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 >}$

Table 5

Fig. 12

Fig. 13

Fig. 14

Table 6

Fig. 15

References 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)))