Modelling and Verification of Multiple UAV Mission Using SMV

Gopinadh Sirigineedi
(Cranfield University, UK)
Antonios Tsourdos
(Cranfield University, UK)
Rafał \.Zbikowski
(Cranfield University, UK)
Brian A. White
(Cranfield University, UK)

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 Computational Tree Logic (CTL). SMV model checker is used for the purpose of model checking.

In Manuela Bujorianu and Michael Fisher: Proceedings FM-09 Workshop on Formal Methods for Aerospace (FMA 2009), Eindhoven, The Netherlands, 3rd November 2009, Electronic Proceedings in Theoretical Computer Science 20, pp. 22–33.
Published: 28th March 2010.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: