Mohammed V University, Rabat, MOROCCO
Farasha Systems and SUPMTI, Rabat, MOROCCO
CADP (Construction and Analysis of Distributed Processes)
Internet of Things.
The Internet of Things (IoT) is the meeting of several technological
fields with the aim of making technology increasingly ubiquitous.
IoT was able to invade home and business applications and began to
access large-scale applications such as transportation and utilities.
Therefore, the IoT must respond to new challenges related to
reliability, dynamicity, and scalability to be able to succeed in
this technological transition from the internet of people to the
internet of things, where things communicate with things or people
to best meet different needs. The IoT system must be reliable to
tolerate errors if certain components are no longer functional.
It must be dynamic in the sense of adding and removing components
during the operation of the system. The IoT system must also be
scalable in order to be deployed in large-scale applications, such
as smart grids.
This work starts by analyzing a typical end-to-end IoT architecture and applies it in a smart grids case study. Then, an architecture named ReDy (Reliable and Dynamic) is proposed for distributed, reliable, dynamic, and scalable IoT systems. The ReDy architecture is hybrid, since it combines centralized and decentralized solutions. The architecture relies on a shuffling algorithm responsible of the membership management of the system nodes. In order to formally validate the criteria of reliability, dynamism, and scalability, the ReDy architecture was formally modeled in LNT, in several configurations. The desired correctness properties of the architecture, focusing on the critical membership management, were expressed as MCL temporal logic formulas, and successfully verified on the various ReDy configurations. The approach was applied to a micro smart grid, which was designed based on the ReDy architecture and was analyzed following the aforementioned formal validation process.
The proposed ReDy architecture and validation methodology, applied to
smart grids, makes it possible to better manage dynamically the
optimization of the production and consumption of energy.
Kaoutar Hafdi, Abdelaziz Kriouile, and Abderahman Kriouile.
"Formal Modeling and Validation of ReDy Architecture Intended for IoT Applications".
International Journal of Innovative Research in Computer Science and
Technology (5):339-349, 2017.
Available on-line at: https://dx.doi.org/10.21276/ijircst.2017.5.4.8
or from the CADP Web site in PDF or PostScript
[Hafdi-20] Kaoutar Hafdi. "Proposition et validation formelle d'une architecture ReDy fiable et dynamique destinée aux systèmes IoT - Application aux Smart Grids". PhD thesis, Université Mohamed V de Rabat, Maroc, November 2020.
Available from the CADP Web site in PDF or PostScript
Département Ingénierie des Systèmes embarqués
Avenue Mohammed Ben Abdallah Regragui
Madinat Al Irfane