Internet of Things design patterns modeling proven correct by construction: Application to aged care solution

• Published in: Future generation computer systems 2023-11, Vol.148, p.395-407
• Main Authors: Tounsi, Imen, Saidi, Abdessamad, Hadj Kacem, Mohamed, Hadj Kacem, Ahmed
• Format: Article
• Language: English
• Subjects: Event-B specifications; Internet of Things; IoT Design patterns; Quality attribute; Smart health monitoring; Software architecture modeling
• ISSN: 0167-739X; 1872-7115
• DOI: 10.1016/j.future.2023.05.018

The Internet of Things (IoT) is a rapidly growing technology trend that seeks to bridge the gap between the physical and digital worlds. Given the complexity of IoT systems, design patterns are essential to overcome recurring problems. However, IoT design patterns must be modeled as valid mathematical entities to avoid implementation errors and ambiguities. This study proposes a refinement-based approach for modeling IoT design patterns using formal method techniques, which enable the creation of correct-by-construction patterns. Our approach uses the Event-B method to specify the models and validate the design. The ultimate goal is to design IoT patterns in a way that ensures their correctness and encourages their reuse. The results of this approach show that it can ensure quality attribute properties while saving time and costs related to software development. We test our approach with examples of patterns and provide a proposed solution in the healthcare sector. This study demonstrates the benefits of using formal methods to model and validate IoT design patterns. •Building Correct-by-Design Internet of Things design patterns.•Patterns are used to develop reliable Internet of Things applications.•Formal specification of the structural and behavioral views of architectures using the Event-B formal method.•Developing an IoT solution in the health care domain that respects the general architecture of the Internet of Things using design patterns.