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 条
  • [1] An DD, Liu J, Chen XH, Sun HY., Formal modeling and dynamic verification for human cyber physical systems under uncertain environment, Ruan Jian Xue Bao/Journal of Software, 32, 7, pp. 1999-2015, (2021)
  • [2] Najm WG, Toma S, Brewer J., Depiction of priority light-vehicle pre-crash scenarios for safety applications based on vehicle-to-vehicle communications, crash causes, (2013)
  • [3] Nitsche P, Thomas P, Stuetz R, Welsh R., Pre-crash scenarios at road junctions: A clustering method for car crash data, Accident Analysis & Prevention, 107, 10, pp. 137-151, (2017)
  • [4] Hauer F, Schmidt T, Holzmuller B, Pretchner A., Did we test all scenarios for automated and autonomous driving systems?, 2019 IEEE Intelligent Transportation Systems Conference (ITSC), pp. 2950-2955, (2019)
  • [5] Ding W, Xu M, Zhao D., Cmts: A conditional multiple trajectory synthesizer for generating safety-critical driving scenarios, 2020 IEEE International Conference on Robotics and Automation (ICRA), pp. 4314-4321, (2020)
  • [6] Paardekooper J, Montfort S, Bracqumond A., Automatic identifification of critical scenarios in a public dataset of 6000 km of public-road driving, Proc. of the 26th International Technical Conference on the Enhanced Safety of Vehicles (ESV), (2019)
  • [7] Zhao Z, Lam H, Peng H, Bao S, LeBlanc DJ, Nobukawa K, Pan CS., Accelerated evaluation of automated vehicles safety in lane-change scenarios based on importance sampling techniques, IEEE Transactions on Intelligent Transportation Systems, 18, 3, pp. 595-607, (2017)
  • [8] Beglerovic H, Stolz M, Horn M., Testing of autonomous vehicles using surrogate models and stochastic optimization, Proc. of the 20th International Conference on Intelligent Transportation Systems (ITSC), pp. 1-6, (2017)
  • [9] Althoff M, Lutz S., Automatic generation of safety-critical test scenarios for collision avoidance of road vehicles, 2018 IEEE Intelligent Vehicles Symposium (IV), pp. 1326-1333, (2018)
  • [10] Klischat M, Althoff M., Generating critical test scenarios for automated vehicles with evolutionary algorithms, 2019 IEEE Intelligent Vehicles Symposium (IV), pp. 2352-2358, (2019)
123