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