Formal Modeling and Validation of ReDy Architecture Intended for IoT Applications

Authors

  • Kaoutar Hafdi IMS Team, ADMIR Laboratory, Rabat IT Center, ENSIAS, Mohammed V University, Rabat, Morocco, Author
  • Abdelaziz Kriouile IMS Team, ADMIR Laboratory, Rabat IT Center, ENSIAS, Mohammed V University, Rabat, Morocco, Author
  • Abderahman Kriouile Farasha Systems, Rabat, Morocco and SUPMTI, Rabat, Morocco Author

Keywords:

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

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]. 

Downloads

Download data is not yet available.

References

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

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

Downloads

Published

2017-07-05

Issue

Vol. 5 No. 4 (2017): International Journal of Innovative Research in Computer Science & Technology(july)2017

Section

Articles

How to Cite

Formal Modeling and Validation of ReDy Architecture Intended for IoT Applications . (2017). International Journal of Innovative Research in Computer Science & Technology, 5(4), 339–349. Retrieved from https://acspublisher.com/journals/index.php/ijircst/article/view/13473