自动驾驶交叉路口测试场景建模及验证方法

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