Formal Validation of ADR Protocol in LoraWan Network Using Event-b

LoRaWAN is a wireless protocol for low-power, wide-area networks (LPWANs). It is a standard protocol for connecting Internet of Things (IoT) devices and sensors over long distances, up to several kilometers, with low power consumption and data rates (DR). LoRaWAN networks are typically implemented in numerous applications, including smart cities, agriculture, logistics, and industrial automation. For this reason, many industrialists and researchers are attempting to develop new protocols for the Lora network. Formal verification can be used to validate the correctness of the protocol implementation to ensure that it conforms to the specification and is free of security vulnerabilities. In the context of the LoRaWAN protocol, Event-B can be used for formal verification by developing a mathematical model of Adaptive Data Rate (ADR) protocol and then refining it to produce an implementation that conforms to the protocol specification. This study aims to build models using formal methods that can efficiently show the complex parts of the ADR protocols server side used in the Lora network to dynamically adjust the up-link and down-link data rates of End Devices and Gateways (GW); by this way, we can detect and fix bugs before implementing the protocol in real scenarios.