On Formal Modeling and Validation of Wireless Sensor Network Protocols
- PDF / 3,183,402 Bytes
- 34 Pages / 439.37 x 666.142 pts Page_size
- 74 Downloads / 179 Views
On Formal Modeling and Validation of Wireless Sensor Network Protocols Rachid Bechar1 · Mounir Tahar Abbes1 · Fareha Mezoudj1 · Ladjel Bellatreche2
© Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Formal verification is becoming more and more important in the field of wireless networks (WSN). The general purpose formal method called Event-B is the latest incarnation of the B Method: it is a proof based approach with a formal notation and refinement technique for modeling and verifying systems. Refinement enables implementation level features to be proven correct with respect to an abstract specification of the system. This paper proposes an initial attempt to model and verify consistency and correctness of a WSN operation in its different layers. Several formal models are introduced for this type of networks. In the first time, coloured Petri net are used to elaborate network layer models, then each one will be detailed by an Event-B formalism, while proofs are carried out using the RODIN platform which is an integrated development framework for Event-B. Keywords WSN · Event-B method · CPN · Formal methods · Validation
1 Introduction Wireless sensor networks (WSN) have a big number of application fields. They are used mainly for environmental sensing, industrial monitoring, target tracking, assisted living and recently internet of things [1]. As a networked system, WSN application needs sensor node as hardware part, operating systems, some networking protocols and the application itself often uses other technologies and techniques such as Ad hoc networks [2], multi-agent systems [3] and data processing [4]. So, its performance depends on all of these factors. Before deploying * Rachid Bechar [email protected] Mounir Tahar Abbes [email protected] Fareha Mezoudj f.mezzoudj@univ‑chlef.dz Ladjel Bellatreche [email protected] 1
Department of Computer Science, FSEI, Hassiba Ben Bouali Uiversity of Chlef, Ouled Fares, Algeria
2
ISAE – ENSMA, University of Poitier, Poitier, France
13
Vol.:(0123456789)
R. Bechar et al.
and installing a WSN, it is imperative to evaluate performances of the new system. There are several methods which can be used for WSN protocols evaluation and validation. The testbed method consists to produce a prototype with a real experimentation, it is the most realistic and complete method but the most costly. For this reason, several works on WSN especially in the academic field use simulation method where protocols are implemented and tested in various simulators like NS2/3 [5], Omnetpp/Castalia [6, 7], Glomosim [8] and J-Sim [9]. However, it is not easy to obtain solid conclusions from a simulation study. This is due to the suitability of a special tool of simulation and correctness of the used models. In addition, using simulators requires an important effort and makes an important time processing. The third way to evaluate performance is emulation which is a compromise between simulation and real testbed. Emulation combines between element
Data Loading...
