| 摘要: |
| 自动驾驶汽车在缓解交通拥堵和消除交通事故方面发挥着重要作用.为了保证自动驾驶系统的安全性和可靠性，在自动驾驶汽车部署到公共道路之前，必须进行全面的测试.现有的测试场景数据大多来源于交通事故和交通违法场景，而且自动驾驶系统最基本的安全需求就是遵守交通法规，这充分体现了自动驾驶汽车遵守交通规则的重要性.然而，目前严重缺少针对交通法规构建的自动驾驶测试场景.因此，从交通法规出发，根据自动驾驶系统的安全需求，提出了交叉路口测试场景的Petri网建模及形式化验证方法.首先，依据自动驾驶测试场景对交规进行分类，提取适合自动驾驶汽车的文本交规，并进行半形式化表征；其次，以覆盖道路交通安全法规以及测试场景功能测试规程为目标，融合交叉路口场景要素的交互行为，合理选择并组合测试场景要素，布设交叉路口测试场景；然后，基于交规的测试场景被建模为一个Petri网，其中，库所描述自动驾驶汽车的状态，变迁表示状态的触发条件，并选择时钟约束规范语言（CCSL）作为中间语义语言，将Petri网转换为一个可进行形式化验证的中间语义模型，提出了具体的转换方法；最后，通过Tina软件分析验证交规场景模型的活性、有界性和可达性，结果表明了所建模型的正确性，并基于SMT的分析工具MyCCSL来分析CCSL约束，采用LTL公式以形式化方法验证交规场景模型的一致性. |
| 关键词: 自动驾驶 测试场景 交规模型 形式化验证 |
| DOI：10.13328/j.cnki.jos.006855 |
| 分类号: |
| 基金项目:牡丹江师范学院国家级课题培育项目（GP2022008）；牡丹江师范学院学科建设揭榜挂帅项目（MSYSYL2022008）；黑龙江省省属高等学校基本科研业务费（1452ZD010）；黑龙江省高等教育教学改革重点委托项目（SJGZ20200175） |
|
| Modeling and Verification Method of Intersection Test Scenario for Automated Driving |
|
XIA Chun-Yan1,2, HUANG Song1, ZHENG Chang-You1, ZHANG Qing-Rui1, WANG Yu1, WEI Yu-Hao1
|
|
1.College of Command and Control Engineering, Army Engineering University of PLA, Nanjing 210007, China;2.College of Computer and Information Technology, Mudanjiang Normal University, Mudanjiang 157012, China
|
| Abstract: |
| 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. Nevertheless, there is a severe lack of test scenarios built for the traffic law. Therefore, in this study, 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, the traffic rules are classified according to the test scenarios of automated driving, the rule text suitable for the autonomous vehicle is extracted and semi-formalized. Secondly, with the aim of covering traffic law and function testing procedure of the test scenario, the interactive behavior of the intersection scene elements is integrated, the typical test scene elements are selected and combined 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, the Clock Constraint Specification Language (CCSL) is chosen 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, Tina is used to verify the activity, boundedness, and accessibility of the traffic-law scenario model, and the experimental results prove the validity of the model. Besides, the CCSL constraints are analyzed through the analysis tool MyCCSL which is based on the SMT and the consistency of the model is verified by the LTL formula. |
| Key words: automated driving test scenario traffic law model formal verification |
