Validating and verifying LwM2M clients with event-B. Issue 2 (5th June 2023)

• Record Type: Journal Article
• Authors: Mouakher, Inès; Dhaou, Fatma; Attiogbé, J. Christian
• Is Part Of: International journal of internet protocol technology. Volume 16:Issue 2(2023)
• Page Start: 75
• Page End: 91
• Publication Date: 2023-06-05
• Subjects: IoT -- internet of things -- lightweight protocols -- device management -- OMA LwM2M -- verification and validation -- V&V -- event-B; File Transfer Protocol (Computer network protocol) -- Periodicals; Multicasting (Computer networks) -- Periodicals; 004.678
• Languages: English
• ISSNs: 1743-8209

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.