自动驾驶软件跨车型部署前，用形式化方法快速验证安全性。
One Stack, Diverse Vehicles: Checking Safe Portability of Automated Driving Software
- 基于安全规范构建不同车辆配置的模型，分析硬件差异影响。
- 几分钟内完成传统与神经网络控制器在多种硬件上的可移植性检查。
- 适合自动驾驶团队做软件更新前的自动化安全验证。
将自动驾驶软件栈集成到配置多样的车辆中极具挑战性，尤其受硬件差异影响。为确保车队在场软件更新的功能安全性，必须验证每个配置下的可靠性。本文提出对自适应巡航控制代码进行形式化可移植性检查，基于安全行为的形式化规范，构建目标配置模型以捕捉传感器、执行器和计算平台的影响。通过生成对应的安全集合，判断所需行为是否能在所有目标上实现。案例研究显示，传统控制器和神经网络控制器的可移植性检查可在每种硬件配置下于几分钟内自动完成，提供必要的控制器调整反馈，从而加速软件或参数变更的集成与测试。
原文摘要 · Abstract (English)
Integrating an automated driving software stack into vehicles with variable configuration is challenging, especially due to different hardware characteristics. Further, to provide software updates to a vehicle fleet in the field, the functional safety of every affected configuration has to be ensured. These additional demands for dependability and the increasing hardware diversity in automated driving make rigorous automatic analysis essential. This paper addresses this challenge by using formal portability checking of adaptive cruise controller code for different vehicle configurations. Given a formal specification of the safe behavior, models of target configurations are derived, which capture relevant effects of sensors, actuators and computing platforms. A corresponding safe set is obtained and used to check if the desired behavior is achievable on all targets. In a case study, portability checking of a traditional and a neural network controller are performed automatically within minutes for each vehicle hardware configuration. The check provides feedback for necessary adaptations of the controllers, thus, allowing rapid integration and testing of software or parameter changes.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。