Semantic Consistency and Correctness Verification of Digital Traffic Rules

作     者：Lei Wan Changjun Wang Daxin Luo Hang Liu Sha Ma Weichao Hu Lei Wan;Changjun Wang;Daxin Luo;Hang Liu;Sha Ma;Weichao Hu

作者机构：PolicyStandardand Patent DepartmentIntelligent Automotive Solution BUHuawei Technologies Co.Ltd.Beijing 100094China Research Institute for Road Safety of the Ministry of Public SecurityBeijing 100062China 

出 版 物：《Engineering》 (工程（英文）)

年 卷 期：2024年第33卷第2期

页      面：47-62页

核心收录：

学科分类：0809[工学-电子科学与技术（可授工学、理学学位）] 08[工学] 

基　　金：Ministry of Public Security and Huawei Technologies Co. Ltd 

主　　题：Autonomous driving Traffic rules Digitization Formalization Verification 

摘      要：The consensus of the automotive industry and traffic management authorities is that autonomous vehicles must follow the same traffic laws as human drivers.Using formal or digital methods,natural language traffic rules can be translated into machine language and used by autonomous vehicles.In this paper,a translation flow is designed.Beyond the translation,a deeper examination is required,because the semantics of natural languages are rich and complex,and frequently contain hidden assumptions.The issue of how to ensure that digital rules are accurate and consistent with the original intent of the traffic rules they represent is both significant and unresolved.In response,we propose a method of formal verification that combines equivalence verification with model checking.Reasonable and reassuring digital traffic rules can be obtained by utilizing the proposed traffic rule digitization flow and verification method.In addition,we offer a number of simulation applications that employ digital traffic rules to assess vehicle violations.The experimental findings indicate that our digital rules utilizing metric temporal logic(MTL)can be easily incorporated into simulation platforms and autonomous driving systems(ADS).