Title: Validating and verifying LwM2M clients with event-B

Authors: Inès Mouakher; Fatma Dhaou; J. Christian Attiogbé

Addresses: Faculty of Sciences of Tunis, University of Tunis El Manar, Tunis, Tunisia ' Faculty of Business Administration, University of Tabuk, Tabuk, Saudi Arabia ' Institute of Technology, University of Nantes, Nantes, France

Abstract: 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.

Keywords: IoT; internet of things; lightweight protocols; device management; OMA LwM2M; verification and validation; V&V; event-B.

DOI: 10.1504/IJIPT.2023.131291

International Journal of Internet Protocol Technology, 2023 Vol.16 No.2, pp.75 - 91

Received: 10 Mar 2021
Accepted: 09 Nov 2021
Published online: 06 Jun 2023 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article