Validating and verifying LwM2M clients with event-B

Lightweight Machine to Machine (LwM2M) is an open industry standard built to provide a means to remotely perform service enablement and application management for the Internet of Things (IoT). It is a communication protocol used between a client software on an IoT device, and a server software. Modelling, formal verification and validation are crucial and necessary to increase protocol reliability. In this paper, we propose a refinement-based approach that helps us to model, to validate and to verify gradually the LwM2M specification, which was carried out using Event-B and Rodin/ProB frameworks. We present a formal model of the LwM2M client, and we verify deadlock freedom and some functional safety properties like consistency of its configuration. The verification is ensured by theorem prover and model checking techniques, and the validation is supported by animation and bounded exploration of the client formal model. Moreover, the transformation into Event-B opens several possibilities to analyse existing implementations of the LwM2M client and to derive both test cases and executable code.