Article
Journal/Revue :
Science of Computer Programming
ISSN : 0167-6423
Publisher :
Informations
Période : October 2022
Volume : 222
Pages : 102859
Détails
Formal Verification of IoT Applications Using Rewriting Logic: An MDE-Based Approach
Abdelouahab Fortas Elhillali Kerkouche Allaoua Chaoui
Internet of Things (IoT) systems are complex assemblies of components that collaborate to achieve common goals. These components are based on heterogeneous technologies, and they communicate using various communication protocols. This heterogeneity makes the design and the development of IoT applications a challenging issue. Diverse approaches based on Model-Driven Engineering (MDE) have been proposed to overcome this major issue using suitable modeling languages. ThingML is a promising UML profile for modeling IoT applications that aims to address the challenges of heterogeneity. However, ThingML does not have rigorous semantics, making it unsuitable for formal verification and analysis of system designs. This paper proposes an MDE-based formal approach to define the formal semantics of the ThingML language using rewriting logic and its language Maude. The main advantage of our approach over other approaches lies in the universality and versatility of Maude's mathematical notation, which implements all ThingML concepts and their behavioral aspects in a unified formal logic. The existing Maude language verification tools provide powerful analysis techniques, including simulation and model checking, which enable rigorous analysis and verification of ThingML designs. The contributions of this work include the following: (i) we propose a semantics mapping between ThingML concepts and Maude constructs, (ii) we define and implement an operational semantics for the ThingML action language in the Maude language, and (iii) we develop a tool that enables the automatic transformation of ThingML specifications into Maude. Our approach is illustrated through a case study.
Mots clés :
Internet of things Formal verification Rewriting logic Model checking Model driven engineering
Réf. de citation :
misc-lab-408
DOI :
https://doi.org/10.1016/j.scico.2022.102859
Lien :
Texte intégral
ACM :
A. Fortas, E. Kerkouche and A. Chaoui. 2022. Formal Verification of IoT Applications Using Rewriting Logic: An MDE-Based Approach. Science of Computer Programming, 222 (October 2022), Elsevier, 102859. DOI: https://doi.org/https://doi.org/10.1016/j.scico.2022.102859.
APA :
Fortas, A., Kerkouche, E. & Chaoui, A. (2022, October). Formal Verification of IoT Applications Using Rewriting Logic: An MDE-Based Approach. Science of Computer Programming, 222, Elsevier, 102859. DOI: https://doi.org/https://doi.org/10.1016/j.scico.2022.102859
IEEE :
A. Fortas, E. Kerkouche and A. Chaoui, "Formal Verification of IoT Applications Using Rewriting Logic: An MDE-Based Approach". Science of Computer Programming, vol. 222, Elsevier, pp. 102859, October, 2022. DOI: https://doi.org/https://doi.org/10.1016/j.scico.2022.102859.
BibTeX :
@article{misc-lab-408,
author = {Fortas, Abdelouahab and Kerkouche, Elhillali and Chaoui, Allaoua},
title = {Formal Verification of IoT Applications Using Rewriting Logic: An MDE-Based Approach},
journal = {Science of Computer Programming},
volume = {222},
issn = {0167-6423},
pages = {102859},
publisher = {Elsevier},
year = {2022},
month = {October},
doi = {https://doi.org/10.1016/j.scico.2022.102859},
url = {https://www.sciencedirect.com/science/article/abs/pii/S0167642322000922},
keywords = {Internet of things, Formal verification, Rewriting logic, Model checking, Model driven engineering}
}
RIS :
TI  - Formal Verification of IoT Applications Using Rewriting Logic: An MDE-Based Approach
AU - A. Fortas
AU - E. Kerkouche
AU - A. Chaoui
PY - 2022
SN - 0167-6423
JO - Science of Computer Programming
VL - 222
SP - 102859
PB - Elsevier
AB - Internet of Things (IoT) systems are complex assemblies of components that collaborate to achieve common goals. These components are based on heterogeneous technologies, and they communicate using various communication protocols. This heterogeneity makes the design and the development of IoT applications a challenging issue. Diverse approaches based on Model-Driven Engineering (MDE) have been proposed to overcome this major issue using suitable modeling languages. ThingML is a promising UML profile for modeling IoT applications that aims to address the challenges of heterogeneity. However, ThingML does not have rigorous semantics, making it unsuitable for formal verification and analysis of system designs. This paper proposes an MDE-based formal approach to define the formal semantics of the ThingML language using rewriting logic and its language Maude. The main advantage of our approach over other approaches lies in the universality and versatility of Maude's mathematical notation, which implements all ThingML concepts and their behavioral aspects in a unified formal logic. The existing Maude language verification tools provide powerful analysis techniques, including simulation and model checking, which enable rigorous analysis and verification of ThingML designs. The contributions of this work include the following: (i) we propose a semantics mapping between ThingML concepts and Maude constructs, (ii) we define and implement an operational semantics for the ThingML action language in the Maude language, and (iii) we develop a tool that enables the automatic transformation of ThingML specifications into Maude. Our approach is illustrated through a case study.
KW - Internet of things
KW - Formal verification
KW - Rewriting logic
KW - Model checking
KW - Model driven engineering
DO - https://doi.org/10.1016/j.scico.2022.102859
UR - https://www.sciencedirect.com/science/article/abs/pii/S0167642322000922
ID - misc-lab-408
ER -