Practical Framework for the Formal Verification of Cooperative Mobile Robots Algorithms

该项目旨在应用模型检查来自动验证多机器人算法的正确性，特别是交会问题。基于我们已经证明的几个重要定理，我们开发了一个验证模型，使我们能够在模型检查器（SPIN）中自动验证给定集合算法的正确性。我们的模型被设计成保守的，如果一个算法A在模型中通过了验证，那么这个算法在现实世界中是正确的，反之则不正确（即使A在模型中失败，在现实世界中也可能是正确的）。在这一年里，我们进一步扩展了验证模型，支持了几个一致性模型，并发现了可以在这些模型中工作的新算法。我们已经将结果作为期刊版本发表，并在开源许可下公开该模型。此外，我们在算法合成方面也取得了进展。简而言之，给定一个系统模型，我们生成所有可能的算法，用几个过滤规则减少搜索空间，只保留那些可行的算法，并用模型检查器检查每个剩余的算法。这使我们能够在可解的模型中找到已知的算法以及新的算法，并部分映射算法存在的已知模型。我们的模型不允许证明不存在性：当一个算法被发现时，它保证是正确的，但是一些正确的算法可能被评估为不正确。

The project aims at applying model checking to automatically verify the correctness of multi-robot algorithms and the problem of rendezvous in particular. Based on several important theorems that we have proved, we have developed a verification model that allows us to automatically verify the correctness of a given rendezvous algorithm in a model-checker (SPIN). Our model is designed to be conservative in the sense that, if an algorithm A passes the verification in the model, then this algorithm is correct in the real-world but the reverse is not true (A could be correct in the real-world even if it fails in the model).During this year, we have further extended the verification model with support for several consistency models and found novel algorithms that can work in these models. We have published the results as a journal version and made the model publicly available under an open-source license.In addition, we have progressed on the front of algorithm synthesis. In short, given a system model, we generate all possible algorithms, reduce the search space with several filtering rules to keep only those that are viable, and check each remaining algorithm with the model checker. This allows us to find known algorithms as well as new ones in models that are solvable, and partially map the known models for the existence of algorithms.Our model does not allow to prove the non-existence: when an algorithm is found it is guaranteed to be correct, but some correct algorithm can possibly be evaluated as incorrect.