形式化行为树的执行上下文以实现慎思策略的运行时验证

在本文中，我们实现了机器人控制架构中慎思组件的自动化属性验证。我们聚焦于形式化行为树（BTs）的执行上下文，以提供可扩展且具形式化基础的方法，从而实现运行时验证并防止意外的机器人行为。为此，我们考虑一种消息传递模型，其容纳并行组件的同步与异步组合，其中BTs与其他组件根据机器人软件架构中通常采用的通信模式执行并交互。我们引入一种形式化属性规约语言以编码需求并构建运行时监视器。我们开展了一组实验，包括仿真与真实机器人，证明了我们的方法在现实应用中的可行性及其在典型机器人软件架构中的集成。我们还提供了一个OS级虚拟化环境以在仿真场景中复现实验。