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

Doctoral Network in Information Technologies and Mathematics

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

1 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Ei tiedossa
Otsikko	Verification and Evaluation of Computer and Communication Systems. VECoS 2017
Toimittajat	K. Barkaoui, H. Boucheneb, A. Mili, Tahar S. (eds)
Kustantaja	Springer
Sivut	189–203
Sivumäärä	15
ISBN (elektroninen)	978-3-319-66176-6
ISBN (painettu)	978-3-319-66175-9
DOI - pysyväislinkit	https://doi.org/10.1007/978-3-319-66176-6_13
Tila	Julkaistu - 2017
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisuussa
Tapahtuma	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 Kesto: 24 elok. 2017 → 25 elok. 2017

Konferenssi

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

Pääsy asiakirjaan

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

Viittausmuodot

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

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

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 - Konferensbidrag

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 -