面向决策、空间与时间的车辆编队模块化验证

自主系统向安全关键领域的普及增加了对其形式化验证的需求，这不仅是出于更严格的认证要求，也是由于公众对这些新技术的疑虑。然而，此类系统的复杂特性（例如离散与连续方面的复杂组合）使得整体系统验证通常不可行。这促使我们需要新的分析方法来对问题进行模块化，允许我们将分析局限于系统的一个特定方面，同时对其他方面进行抽象。例如，在验证自主系统的实时特性时，我们可能会隐藏内部决策组件的细节。在本文中，我们描述了在实用的混合智能体架构上跨不同维度验证一系列属性。这使我们能够验证自主车辆编队系统的自主决策、实时特性和空间特性。这种模块化方法还展示了如何将算法验证和演绎验证技术应用于不同系统子组件的分析。