Practical Framework for the Formal Verification of Cooperative Mobile Robots Algorithms

点击翻译按钮获取中文摘要

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.