Title :
An Abstract Model of a Coordination Protocol Using the UPPAAL Model Checker
Author :
Bhandal, Colm ; Bouroche, Mélanie ; Hughes, Arthur
Author_Institution :
Sch. of Comput. Sci. & Stat., Trinity Coll., Dublin, Ireland
Abstract :
Comhordú is a coordination model for autonomous mobile wireless real time systems. A formalisation of Comhordu is developed using the UPPAAL framework. The formal model is then analysed and simulated, with desirable properties such as system safety machine checked. The formalisation gives us a better understanding of Comhordu and the verification of the LTL formulae supports previous claims as to the correctness of Comhordú.
Keywords :
formal verification; mobile computing; protocols; real-time systems; Comhordu; LTL formulae; UPPAAL model checker; abstract model; autonomous mobile wireless real time systems; coordination protocol; system safety machine; Adaptation models; Analytical models; Automata; Computational modeling; Protocols; Safety; Unified modeling language; Agent; Coordination Protocol; Mobile Computing; Mobile Reactive Systems; Real Time; Safety Properties; UPPAAL model checker; Wireless Networks;
Conference_Titel :
Embedded and Ubiquitous Computing (EUC), 2011 IFIP 9th International Conference on
Conference_Location :
Melbourne, VIC
Print_ISBN :
978-1-4577-1822-9
DOI :
10.1109/EUC.2011.14
