通过Event-B精化对责任感知自动驾驶车辆安全架构的形式化建模
软件工程
2024-01-11 v1
摘要
确保自动驾驶车辆（AV）的安全是其被社会接受的关键前提。在各种交通场景下，用基于AI的黑盒控制器及周围物体来形式化证明其安全条件，其复杂性构成了核心挑战。本文描述了我们在利用Event-B精化机制建模、推导和证明AV安全条件以降低复杂性的策略与经验。我们的案例研究针对最先进的目标感知责任敏感安全模型，以论证与周围车辆的交互。我们还采用Simplex架构以纳入先进的黑盒AI控制器。我们的经验表明，精化机制可有效用于在场景变化下逐步开发复杂系统。
引用
@article{arxiv.2401.04875,
title = {Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement},
author = {Tsutomu Kobayashi and Martin Bondu and Fuyuki Ishikawa},
journal= {arXiv preprint arXiv:2401.04875},
year = {2024}
}
备注
18 pages, 10 figures, author version of the manuscript of the same name published in the proceedings of the 25th International Symposium on Formal Methods (FM 2023)