GoA4级全自动运行系统驾驶模式切换的安全性建模

摘要

为验证具体场景下GoA4级全自动运行系统驾驶模式是否符合对应技术规范,提出一种基于时间自动机的形式化建模与验证方法。GoA4级的驾驶模式是系统自动切换,且增加了自动实现蠕动模式和远程限制监督模式切换。选取全自动运行模式、蠕动模式和远程限制监督模式的相关切换作为建模对象,提取全自动运行系统规范中的功能需求,生成对应流程的消息顺序图,并对模块间的交互信息进行分析;然后,以基于时间自动机的数学理论为基础,采用时间自动机建模方法对RM模式向FAM模式切换、FAM模式向CAM模式切换、FAM模式向RRM模式切换进行建模;最后,采用巴科斯范式(BNF)语法,达到了对其安全性、受限活性、实时性进行验证的结果。