Uppaal vs Event-B for Modelling Optimised Link State Routing

Mojgan Kamali, Luigia Petre

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussaKonferenssiartikkeliTieteellinenvertaisarvioitu

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äiskieliEi tiedossa
OtsikkoVerification and Evaluation of Computer and Communication Systems. VECoS 2017
ToimittajatK. Barkaoui, H. Boucheneb, A. Mili, Tahar S. (eds)
KustantajaSpringer
Sivut189–203
Sivumäärä15
ISBN (elektroninen)978-3-319-66176-6
ISBN (painettu)978-3-319-66175-9
DOI - pysyväislinkit
TilaJulkaistu - 2017
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational 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 elokuuta 201725 elokuuta 2017

Konferenssi

KonferenssiInternational Conference on Verification and Evaluation of Computer and Communication Systems. VECoS
Ajanjakso24/08/1725/08/17

Viittausmuodot