Validating and verifying LwM2M clients with event-B
by Inès Mouakher; Fatma Dhaou; J. Christian Attiogbé
International Journal of Internet Protocol Technology (IJIPT), Vol. 16, No. 2, 2023

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.

Online publication date: Tue, 06-Jun-2023

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Internet Protocol Technology (IJIPT):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com