Provably-Correct Compositional Synthesis of Vehicle Safety Systems
Provably-Correct Compositional Synthesis of Vehicle Safety Systems
复制标题
可证明正确的车辆安全系统组合综合
DOI：
10.1007/978-3-319-97301-2_6
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
N. Ozay
中科院分区：
文献类型：
--
作者：
Petter Nilsson;N. Ozay
随着汽车朝着完全自动驾驶的方向发展，许多驾驶便利和安全自动化系统被引入到生产车辆中。这些系统通常包括为个别任务设计的控制器。为相互作用的子系统设计单独的控制器，并以一种保留每个控制器对每个子系统提供的保证的方式组成它们，是一项具有挑战性的任务。本章介绍了通过使用形式化方法和逐结构校正控制器综合来解决这个问题的最新结果。讨论了用于处理实现和模型缺陷的机制，以及基于契约的功能组合。这些想法在CarSim的高保真模拟中得到了展示，在密歇根大学自动驾驶车辆测试设施MCity的真实车辆上也得到了展示。
As the automobile evolves toward full autonomy, many driver convenience and safety automation systems are being introduced into production vehicles. These systems often include controllers designed for individual tasks. Designing individual controllers for interacting subsystems, and composing them in a way that preserves the guarantees that each controller provides on each subsystem, is a challenging task. This chapter presents recent results addressing this problem through the use of formal methods and correct-by-construction controller synthesis. Mechanisms for handling implementation- and model imperfections, and contract-based composition of functionality, are discussed. The ideas are demonstrated in high-fidelity simulations in CarSim, and also on a real vehicle in Mcity, the autonomous vehicle testing facility at the University of Michigan.