Formal modelling of the Friendship mechanism in Bluetooth Mesh
2023
The emergence of Bluetooth Low Energy has brought about a huge revolution, which has been further augmented by the release of Bluetooth Low EnergyMesh. Despite its rapid adoption, there are still challenges to overcome, with power consumption being considered one of themost important issues as the node’s battery life depends on it. The standard configuration of BLEmesh is not energy-efficient, since it operates in an always-on, always-listening, and always-communicatingmode, which is not suitable for power-limited devices. To address this issue, the standard includes the Friendshipmechanism, which is a key factor in extending battery life. In this paper, we present the formalmodel of the Friendshipmechanismdeveloped using Coloured Petri Nets. Thismodel is analysed using state space techniques to determine the correctness properties, as well as the absence of deadlocks and proper termination. Our model allows us to verify the algorithm before its implementation and to evaluate its performance before its deployment in a real environment. In addition, the formalmodel will be useful for future improvements and for evaluating possible alternatives based on the system’s requirements. Ourmodel has been validated using data obtained fromthe testbed deployed in our laboratory.