Formal Modeling and Validation of ReDy Architecture Intended for IoT Applications

Kaoutar Hafdi; Abdelaziz Kriouile; Abderahman Kriouile

Abstract

Internet of Things (IoT) faces different architectural challenges to meet the large scale application issues, the heterogeneity, and the self-adaptivity. Many IoT applications require a dynamic construction of the system and should ensure a high degree of reliability. To this end, we propose the ReDy architecture [1], which is a reusable solution for reliable and dynamic distributed IoT applications. In this paper we propose a formalization and validation of the ReDy architecture. For this end, we propose a formal model using LNT language [2]. We propose also a suitable algorithm to implement a reliable and dynamic membership management. Then we give a formal validation of this critical part based on formal modeling and model checking techniques [3].

Keywords

Internet of Things (IoT), Distributed systems, Formal methods

References

[1] K. Hafdi and A. Kriouile, “Designing redy distributed systems,” in Autonomic Computing (ICAC), 2015 IEEE International Conference on. IEEE, 2015, pp. 331–336.

[2] D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, V. Powazny, F. Lang, W. Serwe, and G. Smeding, “Reference manual of the lnt to lotos translator (version 6.1),” Inria/Vasy and Inria/Convecs, vol. 131, 2014.

[3] R. Mateescu and D. Thivolle, “A model checking language for con-current value-passing systems,” inInternational Symposium on Formal Methods. Springer, 2008, pp. 148–164.

[4] A. P. Castellani, N. Bui, P. Casari, M. Rossi, Z. Shelby, and M. Zorzi, “Architecture and protocols for the internet of things: A case study,” in Pervasive Computing and Communications Workshops (PERCOM Workshops), 2010 8th IEEE International Conference on. IEEE, 2010, pp. 678–683.

[5] J. Gubbi, R. Buyya, S. Marusic, and M. Palaniswami, “Internet of things (iot): A vision, architectural elements, and future directions,” Future generation computer systems, vol. 29, no. 7, pp. 1645–1660, 2013.

[6] H. Garavel, F. Lang, R. Mateescu, and W. Serwe, “CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes,” in Proc. of STTT’13. Springer, 2013.

[7] E. K. Lua, J. Crowcroft, M. Pias, R. Sharma, S. Lim et al., “A survey and comparison of peer-to-peer overlay network schemes.”IEEE Communications Surveys and Tutorials, vol. 7, no. 1-4, pp. 72–93, 2005.

[8] A. Tanenbaum and M. Van Steen, Distributed systems. Pearson Prentice Hall, 2007.

[9] S. Voulgaris, D. Gavidia, and M. Van Steen, “Cyclon: Inexpensive membership management for unstructured p2p overlays,”Journal of Network and Systems Management, vol. 13, no. 2, pp. 197–217, 2005.

[10] M. Jelasity, R. Guerraoui, A.-M. Kermarrec, and M. Van Steen, “The peer sampling service: Experimental evaluation of unstructured gossip-based implementations,” inProceedings of the 5th ACM/IFIP/USENIX international conference on Middleware. Springer-Verlag New York, Inc., 2004, pp. 79–98.

[11] M. Jelasity, S. Voulgaris, R. Guerraoui, A.-M. Kermarrec, and M. Van Steen, “Gossip-based peer sampling,”ACM Transactions on Computer Systems (TOCS), vol. 25, no. 3, p. 8, 2007.

[12] R. Guerraoui, R. Oliveira, and A. Schiper, “Stubborn communication channels,” Tech. Rep., 1998.

[13] C. Cachin, R. Guerraoui, and L. Rodrigues,Introduction to reliable and secure distributed programming. Springer, 2011.

[14] T. A. Henzinger, “The theory of hybrid automata,” in Verification of Digital and Hybrid Systems. Springer, 2000, pp. 265–292.

[15] H. Balakrishnan, M. F. Kaashoek, D. Karger, R. Morris, and I. Stoica, “Looking up data in p2p systems,”Communications of the ACM, vol. 46, no. 2, pp. 43–48, 2003.

[16] I. Stoica, R. Morris, D. Liben-Nowell, D. R. Karger, M. F. Kaashoek, F. Dabek, and H. Balakrishnan, “Chord: a scalable peer-to-peer lookup protocol for internet applications,” Networking, IEEE/ACM Transac-tions on, vol. 11, no. 1, pp. 17–32, 2003.

[17] I. Demirkol, C. Ersoy, and F. Alagoz, “Mac protocols for wireless sensor networks: a survey,”IEEE Communications Magazine, vol. 44, no. 4, pp. 115–121, 2006.

[18] Kriouile and W. Serwe, “Formal analysis of the ace specification for cache coherent systems-on-chip,” inInternational Workshop on Formal Methods for Industrial Critical Systems. Springer, 2013, pp. 108–122.

[19] A. Kriouile and W. Serwe, “Using a formal model to improve verification of a cache-coherent system-on-chip,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2015, pp. 708–722.

Cites this article as

K. Hafdi, A. Kriouile, A. Kriouile, "Formal Modeling and Validation of ReDy Architecture Intended for IoT Applications", International Journal of Innovative Research in Computer Science and Technology (IJIRCST), Vol-5, no.4, pp.339-349, 2017. Available from: https://search.crossref.org/?q=10.21276%2Fijircst.2017.5.4.8

Corresponding Author

Kaoutar Hafdi

IMS Team, ADMIR Laboratory, Rabat IT Center, ENSIAS, Mohammed V University, Rabat, Morocco,

Download Full Paper

Download PDF

No. of Downloads: 9 | No. of Views: 1106

IJIRCST

Formal Modeling and Validation of ReDy Architecture Intended for IoT Applications

Citations

Download Full Paper PDF

Total View 1106

Total Download 9