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

Doctoral Network in Information Technologies and Mathematics

Research output: Chapter in Book/Conference proceeding › Published conference proceeding › Scientific › peer-review

1 Citation (Scopus)

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.

Original language	Undefined/Unknown
Title of host publication	Verification and Evaluation of Computer and Communication Systems. VECoS 2017
Editors	K. Barkaoui, H. Boucheneb, A. Mili, Tahar S. (eds)
Publisher	Springer
Pages	189–203
Number of pages	15
ISBN (Electronic)	978-3-319-66176-6
ISBN (Print)	978-3-319-66175-9
DOIs	https://doi.org/10.1007/978-3-319-66176-6_13
Publication status	Published - 2017
MoE publication type	A4 Article in a conference publication
Event	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 Duration: 24 Aug 2017 → 25 Aug 2017

Conference

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

Access to Document

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

Cite this

@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. in K Barkaoui, H Boucheneb, A Mili & TS (eds) (eds), Verification and Evaluation of Computer and Communication Systems. VECoS 2017. Springer, pp. 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. ed. / K. Barkaoui; H. Boucheneb; A. Mili; Tahar S. (eds). Springer, 2017. p. 189–203.

Research output: Chapter in Book/Conference proceeding › Published conference proceeding › Scientific › 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 -