Modeling and Validation of ReDy Architecture for IoT Applications

Organisation:	Mohammed V University, Rabat, MOROCCO Farasha Systems and SUPMTI, Rabat, MOROCCO
Method:	LNT MCL
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Internet of Things.
Period:	2017-2020
Size:	n/a
Description:	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.
Conclusions:	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.
Publications:	[Hafdi-Kriouile-17] 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 [Hafdi-Kriouile-20] Kaoutar Hafdi and Abderahman Kriouile. "Formal Modeling and Validation of Micro Smart Grids Based on ReDy Architecture". Proc. of the 5th International Conference on Cloud Computing and Artificial Intelligence: Technologies and Applications (CloudTech'2020), Marrakesh, Morocco, pp. 1-7. IEEE CS Press, 2020. Available on-line at: https://doi.org/10.1109/CloudTech49835.2020.9365923 or from the CADP Web site in PDF or PostScript
Contact:	Abderahman Kriouile ENSIAS Département Ingénierie des Systèmes embarqués Avenue Mohammed Ben Abdallah Regragui Madinat Al Irfane BP 713 Agdal Rabat MAROC Email: a.kriouile@um5s.net.ma

Back to the CADP case studies page