软件学报

作者：夏春艳，黄松，郑长友，张清睿，王宇，魏瑀皓

单位：夏春艳，中国人民解放军陆军工程大学 指挥控制工程学院, 江苏 南京 210007;牡丹江师范学院 计算机与信息技术学院, 黑龙江 牡丹江 15701211,黄松，中国人民解放军陆军工程大学 指挥控制工程学院, 江苏 南京 21000702,郑长友，中国人民解放军陆军工程大学 指挥控制工程学院, 江苏 南京 21000703,张清睿，中国人民解放军陆军工程大学 指挥控制工程学院, 江苏 南京 21000704,王宇，中国人民解放军陆军工程大学 指挥控制工程学院, 江苏 南京 21000705,魏瑀皓，中国人民解放军陆军工程大学 指挥控制工程学院, 江苏 南京 21000706

关键词：自动驾驶;测试场景;交规模型;形式化验证

基金：牡丹江师范学院国家级课题培育项目（GP2022008）；牡丹江师范学院学科建设揭榜挂帅项目（MSYSYL2022008）；黑龙江省省属高等学校基本科研业务费（1452ZD010）；黑龙江省高等教育教学改革重点委托项目（SJGZ20200175）

自动驾驶汽车在缓解交通拥堵和消除交通事故方面发挥着重要作用.为了保证自动驾驶系统的安全性和可靠性，在自动驾驶汽车部署到公共道路之前，必须进行全面的测试.现有的测试场景数据大多来源于交通事故和交通违法场景，而且自动驾驶系统最基本的安全需求就是遵守交通法规，这充分体现了自动驾驶汽车遵守交通规则的重要性.然而，目前严重缺少针对交通法规构建的自动驾驶测试场景.因此，从交通法规出发，根据自动驾驶系统的安全需求，提出了交叉路口测试场景的Petri网建模及形式化验证方法.首先，依据自动驾驶测试场景对交规进行分类，提取适合自动驾驶汽车的文本交规，并进行半形式化表征；其次，以覆盖道路交通安全法规以及测试场景功能测试规程为目标，融合交叉路口场景要素的交互行为，合理选择并组合测试场景要素，布设交叉路口测试场景；然后，基于交规的测试场景被建模为一个Petri网，其中，库所描述自动驾驶汽车的状态，变迁表示状态的触发条件，并选择时钟约束规范语言（CCSL）作为中间语义语言，将Petri网转换为一个可进行形式化验证的中间语义模型，提出了具体的转换方法；最后，通过Tina软件分析验证交规场景模型的活性、有界性和可达性，结果表明了所建模型的正确性，并基于SMT的分析工具MyCCSL来分析CCSL约束，采用LTL公式以形式化方法验证交规场景模型的一致性.

来源：2023年第7期

《软件学报》期刊编辑部

查看软件学报杂志2023年第7期