基于可达性分析的机器人接触任务形式化验证

由于与接触相关的模型不确定性，验证机器人在接触任务中的正确行为具有挑战性。标准的测试方法往往不足，因为无法获得所有（不可数无穷多）解。相反，我们提出使用可达性分析对接触任务中的机器人行为进行有效形式化验证，从而能够针对用户提供的规范检查所有可达状态。为此，我们拓展了针对受离散时间输入轨迹影响的混合（离散与连续混合）动力学可达性分析的现状。特别地，我们提出了一种新颖且可扩展的守卫交集方法，以可靠地计算由接触引起的复杂行为。我们将受接触影响的机器人建模为包含关键时间延迟的混合自动机。通过在存在受限碰撞的情况下验证安全的人机交互，证明了我们方法的有效性，这是现有方法无法做到的。