• DocumentCode
    2665866
  • 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
  • fYear
    2011
  • fDate
    24-26 Oct. 2011
  • Firstpage
    306
  • Lastpage
    311
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Embedded and Ubiquitous Computing (EUC), 2011 IFIP 9th International Conference on
  • Conference_Location
    Melbourne, VIC
  • Print_ISBN
    978-1-4577-1822-9
  • Type

    conf

  • DOI
    10.1109/EUC.2011.14
  • Filename
    6104542