使用NuXMV和GROOVE对Alpha Swarm算法进行规范化和验证

《Formal Aspects of Computing》：Specification and Verification of the Alpha Swarm Algorithm using NuXMV and GROOVE

群体机器人系统通过分布式协作实现共同目标，但缺乏中央控制器导致个体行为与群级目标一致性验证困难。本文提出两种形式化验证框架：NuXMV将系统建模为有限状态机，使用时态逻辑进行规格说明，并借助BDDs和SMT求解器进行模型检查；GROOVE采用图文法建模，结合图形状态时态逻辑，通过专用图模型检查算法验证。通过Alpha群集算法建模对比发现，GROOVE能有效利用对称性缩减状态空间，而NuXMV在复杂计算和数据处理方面更优。讨论了不同系统场景下两种方法的适用性，并指出未来结合优势的改进方向。

　　

摘要

群体机器人系统由众多简单的机器人组成，这些机器人以分散的方式协作以实现共同的目标。由于缺乏中央控制器，确保单个机器人的行为能够产生期望的群体级结果是具有挑战性的。本文使用了两种框架来促进机器人群体的形式化规范和验证：1) NuXMV，它将系统建模为有限状态机，使用时态逻辑指定属性，并通过BDD（行为驱动开发）和SMT（符号模型检测）求解器进行模型验证；2) GROOVE，它将系统建模为图语法，使用带有图形状态的时态逻辑指定属性，并通过特定于图的模型检测算法进行验证。我们通过建模Alpha群体聚合算法来比较这两种形式化方法，该算法确保任何与群体断开连接的机器人（仅能进行短距离无线通信）最终都会重新加入群体。我们发现GROOVE能够有效利用对称性来减少状态空间，而NuXMV在处理需要大量计算和数据操作的模型时表现出色，这些操作无法通过图来最优地表达。我们讨论了每种方法适用于不同系统和属性的情况，并提出了结合两种方法优势的未来研究方向。