Modelling and Verification of Multiple UAV Mission Using SMV

Modelling and Verification of Multiple UAV Mission Using 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 aime...

Full description

Bibliographic Details
Main Authors: Gopinadh Sirigineedi, Antonios Tsourdos, Rafał Żbikowski, Brian A. White
Format: Article
Language:English
Published: Open Publishing Association 2010-03-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1003.0381v1
id doaj-39f7f7cb53af4f9d9f6c494f8337bd4c
record_format Article
spelling doaj-39f7f7cb53af4f9d9f6c494f8337bd4c2020-11-24T23:34:39ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-03-0120Proc. FMA 2009223310.4204/EPTCS.20.3Modelling and Verification of Multiple UAV Mission Using SMVGopinadh SirigineediAntonios TsourdosRafał ŻbikowskiBrian A. WhiteModel 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. http://arxiv.org/pdf/1003.0381v1
collection DOAJ
language English
format Article
sources DOAJ
author Gopinadh Sirigineedi
Antonios Tsourdos
Rafał Żbikowski
Brian A. White
spellingShingle Gopinadh Sirigineedi
Antonios Tsourdos
Rafał Żbikowski
Brian A. White
Modelling and Verification of Multiple UAV Mission Using SMV
Electronic Proceedings in Theoretical Computer Science
author_facet Gopinadh Sirigineedi
Antonios Tsourdos
Rafał Żbikowski
Brian A. White
author_sort Gopinadh Sirigineedi
title Modelling and Verification of Multiple UAV Mission Using SMV
title_short Modelling and Verification of Multiple UAV Mission Using SMV
title_full Modelling and Verification of Multiple UAV Mission Using SMV
title_fullStr Modelling and Verification of Multiple UAV Mission Using SMV
title_full_unstemmed Modelling and Verification of Multiple UAV Mission Using SMV
title_sort modelling and verification of multiple uav mission using smv
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2010-03-01
description 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.
url http://arxiv.org/pdf/1003.0381v1
work_keys_str_mv AT gopinadhsirigineedi modellingandverificationofmultipleuavmissionusingsmv
AT antoniostsourdos modellingandverificationofmultipleuavmissionusingsmv
AT rafałzbikowski modellingandverificationofmultipleuavmissionusingsmv
AT brianawhite modellingandverificationofmultipleuavmissionusingsmv
_version_ 1725528220054323200

Similar Items