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.
Key words :
Internet of things
Formal verification
Rewriting logic
Model checking
Model driven engineering
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 -