Uppaal vs Event-B for Modelling Optimised Link State Routing

A4 Konferenspublikationer


Interna författare/redaktörer


Publikationens författare: Mojgan Kamali, Luigia Petre
Redaktörer: Barkaoui K., Boucheneb H., Mili A., Tahar S. (eds)
Förläggare: SPRINGER INTERNATIONAL PUBLISHING AG, GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND
Publiceringsår: 2017
Förläggare: Springer
Moderpublikationens namn: Verification and Evaluation of Computer and Communication Systems. VECoS 2017
Tidskriftsakronym: LECT NOTES COMPUT SC
Seriens namn: Lecture Notes in Computer Science (LNCS)
Volym: 10466
Artikelns första sida, sidnummer: 189
Artikelns sista sida, sidnummer: 203
Antal sidor: 15
ISBN: 978-3-319-66175-9
eISBN: 978-3-319-66176-6
ISSN: 0302-9743


Abstrakt

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.

Senast uppdaterad 2019-15-09 vid 07:45