Modelling and Verification of Multiple UAV Mission Using SMV
Modelling and Verification of Multiple UAV Mission Using SMV
复制标题
使用 SMV 的多无人机任务建模和验证
DOI：
10.4204/eptcs.20.3
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
R. Zbikowski
中科院分区：
文献类型：
--
作者：
G. Sirigineedi;A. Tsourdos;B. White;R. Zbikowski
模型检测已被用于验证数字电路、安全协议、通信协议的正确性，因为它们可以通过有限状态转换模型来建模。然而，在克里普克模型中对诸如无人机等混合系统的行为进行建模是具有挑战性的。这项工作旨在将执行协同搜索任务的无人机的行为捕捉到一个克里普克模型中，以便根据计算树逻辑（CTL）中表达的时态属性对其进行验证。为此目的，使用SMV模型检验器进行模型检测。
Model checking has been used to verify the correctness of digital circuits, security protocols, communication protocols, as they can be modelled by means of finite state transition model. However, modelling the behaviour of hybrid systems like UAVs in a Kripke model is challenging. This work is aimed at capturing the behaviour of an UAV performing cooperative search mission into a Kripke model, so as to verify it against the temporal properties expressed in Computation Tree Logic (CTL). SMV model checker is used for the purpose of model checking.