Modeling and Verification Method of Intersection Test Scenario for Automatic Driving

被引：0

作者：

Xia C.-Y. ^{[1
,2
]}

Huang S. ^{[1
]}

Zheng C.-Y. ^{[1
]}

Zhang Q.-R. ^{[1
]}

Wang Y. ^{[1
]}

Wei Y.-H. ^{[1
]}

机构：

[1] College of Command and Control Engineering, Army Engineering University, PLA, Nanjing

[2] Collegeof Computer and Information Technology, Mudanjiang Normal University, Mudanjiang

来源：

Ruan Jian Xue Bao/Journal of Software | 2023年 / 34卷 / 07期

关键词：

automatic driving; formal verification; test scenario; traffic law model;

D O I：

10.13328/j.cnki.jos.006855

中图分类号：

学科分类号：

摘要：

Autonomous vehicles play an important role in easing traffic congestion and eliminating traffic accidents. In order to ensure the safety and reliability of the autonomous vehicle, there must be an all-around test before they are deployed on public roads. Most of the existing test scenario data come from traffic accidents and traffic violations, furthermore, the most fundamental safety requirement of an autopilot system is that autonomous vehicles should comply with traffic law, which fully reflects the importance of autonomous vehicles complying with traffic rules. However, there is a severe lack of test scenarios built for the traffic law. Therefore, in this paper, the safety requirements of the autopilot system are extracted from the traffic law perspective, and a Petri net modeling and formal verification method for intersection test scenarios is proposed. Firstly, we classify the traffic rules according to the test scenarios of automatic driving, extract and semi-formalize the rule text suitable for the autonomous vehicle. Secondly, with the aim of covering traffic law and function testing procedure of the test scenario, we integrate the interactive behavior of the intersection scene elements, select and combine the typical test scene elements to deploy the intersection test scenarios. Then, the test scenario based on traffic rules is modeled as a Petri net, in which places describe the state of the autonomous vehicle and transitions represent the trigger condition of the state. Moreover, we choose Clock Constraint Specification Language(CCSL) as the intermediate semantic language to convert the Petri net into an intermediate semantic model which can be formally verified. A specific conversion method is proposed. Finally, we use Tina to verify the activity, boundedness and accessibility of the traffic-law scenario model，and the experimental results prove the validity of the model. Besides，we analyze the CCSL constraints through the analysis tool MyCCSL which is based on the SMT and verify the consistency of the model by the LTL formula. © 2023 Chinese Academy of Sciences. All rights reserved.

引用

共 21 条

[11] Zhu XL, Wang HC, You HM, Zhang WH, Zhang YY, Liu S, Chen JJ, Wang Z, Li KQ., Survey on testing of intelligent systems in autonomous vehicles, Ruan Jian Xue Bao/Journal of Software, 32, 7, pp. 2056-2077, (2021)
[12] Kumar SSV., Intersection Collision Avoidance for Autonomous Vehicles Using Petri Nets, (2019)
[13] Tang Y, Zhou Y, Wu F, Liu Y, Sun J, Huang W, Wang G., Route coverage testing for autonomous vehicles via map modeling, 2021 IEEE International Conference on Robotics Automation(ICRA), pp. 11450-11456, (2021)
[14] Lima V, Talhi C, Mouheb D, Debbabi M, Wang L, Pourzandi M., Formal verifification and validation of UML 2.0 sequence diagrams using source and destination of messages, Electronic Notes in Theoretical Computer Science, 254, 1, pp. 143-160, (2009)
[15] Han D, Xing J, Yang Q, Wang H, Zhang X., Formal sequence: extending UML eequence diagram for behavior description and formal verification, 40th IEEE Annual Computer Software and Applications Conference, pp. 474-481, (2016)
[16] Soares JAC, Lima B, Faria JP., Automatic model transformation from UML sequence diagrams to coloured petri nets, Proceedings of the 6th International Conference on Model-Driven Engineering and Software Development, pp. 668-679, (2018)
[17] Petri C, Reisig W., Petri net, Scholarpedia, 3, 1, pp. 133-136, (2008)
[18] Liu G., Petri Nets: Theoretical Models and Analysis Methods for Concurrent Systems, (2022)
[19] He L, Liu G., LF He, GJ Liu, Prioritized time-point-interval Petri nets modeling multi-processor real-time systems and TCTLx, IEEE Transactions on Industrial Informatics, (2022)
[20] Gascon R, Mallet F, Deantoni J., Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL, Proc. of the 18th International Symposium on Temporal Representation and Reasoning, (2011)

← 1 2 3 →