论文标题
通过设计协调自动驾驶系统的设计
Correct by Design Coordination of Autonomous Driving Systems
论文作者
论文摘要
本文提出了一种通过设计自主驾驶系统（ADS）的设计协调来正确的方法。它以先前的结果为基础，以避免碰撞策略和广告的建模，通过将其静态环境的描述和车辆的动态行为结合在一起。广告被建模为一个动态系统，该系统涉及一组由运行时协调的车辆，该车辆基于地图上的车辆位置及其动力学属性，为每个车辆计算免费空间。车辆有限，以在相应的分配自由空间内移动。如果其车辆和运行时尊重相应的假定保证合同，我们通过设计安全控制政策提供了正确的正确控制政策。通过证明假设合同的组成是需要ADS安全的归纳不变的，从而确定了结果。我们表明，实际上可以为符合其合同的车辆定义速度控制政策。此外，我们表明可以在线性时间逻辑中指定流量规则为限制车辆速度的一类公式。主要结果是，鉴于一组流量规则，可以得出运行时的可用空间策略，从而通过设计相对于规则而设计的系统行为是安全的。
The paper proposes a method for the correct by design coordination of autonomous driving systems (ADS). It builds on previous results on collision avoidance policies and the modeling of ADS by combining descriptions of their static environment in the form of maps, and the dynamic behavior of their vehicles. An ADS is modeled as a dynamic system involving a set of vehicles coordinated by a Runtime that based on vehicle positions on a map and their kinetic attributes, computes free spaces for each vehicle. Vehicles are bounded to move within the corresponding allocated free spaces. We provide a correct by design safe control policy for an ADS if its vehicles and the Runtime respect corresponding assume-guarantee contracts. The result is established by showing that the composition of assume-guarantee contracts is an inductive invariant that entails ADS safety. We show that it is practically possible to define speed control policies for vehicles that comply with their contracts. Furthermore, we show that traffic rules can be specified in a linear-time temporal logic, as a class of formulas that constrain vehicle speeds. The main result is that, given a set of traffic rules, it is possible to derive free space policies of the Runtime such that the resulting system behavior is safe by design with respect to the rules.
