Uppaal vs Event-B for Modelling Optimised Link State Routing

Mojgan Kamali; Luigia Petre

doi:10.1007/978-3-319-66176-6_13

Uppaal vs Event-B for Modelling Optimised Link State Routing

Mojgan Kamali, Luigia Petre

Doktorandnätverk IT and Mathematics

Forskningsoutput: Kapitel i bok/konferenshandling › Publicerad konferensartikel › Vetenskaplig › Peer 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åk	Odefinierat/okänt
Titel på värdpublikation	Verification and Evaluation of Computer and Communication Systems. VECoS 2017
Redaktörer	K. Barkaoui, H. Boucheneb, A. Mili, Tahar S. (eds)
Förlag	Springer
Sidor	189–203
Antal sidor	15
ISBN (elektroniskt)	978-3-319-66176-6
ISBN (tryckt)	978-3-319-66175-9
DOI	https://doi.org/10.1007/978-3-319-66176-6_13
Status	Publicerad - 2017
MoE-publikationstyp	A4 Artikel i en konferenspublikation
Evenemang	International 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. 2017 → 25 aug. 2017

Konferens

Konferens	International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS
Period	24/08/17 → 25/08/17

Åtkomst av dokument

10.1007/978-3-319-66176-6_13

Citera det här

@inproceedings{13f8e4b74c57410e82874411870dbbfe,

title = "Uppaal vs Event-B for Modelling Optimised Link State Routing",

abstract = "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.",

author = "Mojgan Kamali and Luigia Petre",

year = "2017",

doi = "10.1007/978-3-319-66176-6_13",

language = "Odefinierat/ok{\"a}nt",

isbn = "978-3-319-66175-9",

pages = "189–203",

editor = "K. Barkaoui and H. Boucheneb and A. Mili and (eds), {Tahar S.}",

booktitle = "Verification and Evaluation of Computer and Communication Systems. VECoS 2017",

publisher = "Springer",

note = "International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS ; Conference date: 24-08-2017 Through 25-08-2017",

}

Kamali, M & Petre, L 2017, Uppaal vs Event-B for Modelling Optimised Link State Routing. i K Barkaoui, H Boucheneb, A Mili & TS (eds) (red), Verification and Evaluation of Computer and Communication Systems. VECoS 2017. Springer, s. 189–203, International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS, 24/08/17. https://doi.org/10.1007/978-3-319-66176-6_13

Uppaal vs Event-B for Modelling Optimised Link State Routing. / Kamali, Mojgan; Petre, Luigia.
Verification and Evaluation of Computer and Communication Systems. VECoS 2017. red. / K. Barkaoui; H. Boucheneb; A. Mili; Tahar S. (eds). Springer, 2017. s. 189–203.

Forskningsoutput: Kapitel i bok/konferenshandling › Publicerad konferensartikel › Vetenskaplig › Peer review

TY - GEN

T1 - Uppaal vs Event-B for Modelling Optimised Link State Routing

AU - Kamali, Mojgan

AU - Petre, Luigia

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-66176-6_13

DO - 10.1007/978-3-319-66176-6_13

M3 - Publicerad konferensartikel

SN - 978-3-319-66175-9

SP - 189

EP - 203

BT - Verification and Evaluation of Computer and Communication Systems. VECoS 2017

A2 - Barkaoui, K.

A2 - Boucheneb, H.

A2 - Mili, A.

A2 - (eds), Tahar S.

PB - Springer

T2 - International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS

Y2 - 24 August 2017 through 25 August 2017

ER -