Uppaal vs Event-B for Modelling Optimised Link State Routing

Mojgan Kamali, Luigia Petre

Forskningsoutput: Kapitel i bok/konferenshandlingKonferensbidragVetenskapligPeer review

1 Citeringar (Scopus)

Sammanfattning

In this paper we compare models developed in two formal frameworks, Uppaal and Event-B, for the Optimised Link State Routing (OLSR) protocol. OLSR is one of the proactive routing protocols used in Mobile Ad-hoc Networks (MANETs) and Wireless Mesh Networks (WMNs). We also describe different aspects of the Uppaal and Event-B formalisms. This leads to a more general comparison of both formalisms, considering the following criteria: their specification languages, their update of variables mechanism, their modularity methods, their verification strategies, their scalability potentials and their real-time modelling capabilities. Based on it, we provide several guidelines for when to use Uppaal or Event-B for formal modelling and analysis.
OriginalspråkOdefinierat/okänt
Titel på gästpublikationVerification and Evaluation of Computer and Communication Systems. VECoS 2017
RedaktörerK. Barkaoui, H. Boucheneb, A. Mili, Tahar S. (eds)
FörlagSpringer
Sidor189–203
Antal sidor15
ISBN (elektroniskt)978-3-319-66176-6
ISBN (tryckt)978-3-319-66175-9
DOI
StatusPublicerad - 2017
MoE-publikationstypA4 Artikel i en konferenspublikation
EvenemangInternational Conference on Verification and Evaluation of Computer and Communication Systems. VECoS - 11th International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS 2017
Varaktighet: 24 aug 201725 aug 2017

Konferens

KonferensInternational Conference on Verification and Evaluation of Computer and Communication Systems. VECoS
Period24/08/1725/08/17

Citera det här