• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Uppaal vs Event-B for Modelling Optimised Link State Routing

Mojgan Kamali, Luigia Petre, Uppaal vs Event-B for Modelling Optimised Link State Routing. In: K. Barkaoui, H. Boucheneb, A. Mili, S. Tahar (Eds.), Verification and Evaluation of Computer and Communication Systems. VECoS 2017, Lecture Notes in Computer Science 10466, 189–203, Springer, 2017.

http://dx.doi.org/10.1007/978-3-319-66176-6_13

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.

BibTeX entry:

@INPROCEEDINGS{inpKaPe17a,
  title = {Uppaal vs Event-B for Modelling Optimised Link State Routing},
  booktitle = {Verification and Evaluation of Computer and Communication Systems. VECoS 2017},
  author = {Kamali, Mojgan and Petre, Luigia},
  volume = {10466},
  series = {Lecture Notes in Computer Science},
  editor = {Barkaoui, K. and Boucheneb, H. and Mili, A. and Tahar, S.},
  publisher = {Springer},
  pages = {189–203},
  year = {2017},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication