Abstract

In this paper, we have described the research carried out in formal modeling of distributed networks in a process algebraic framework. The extended version of asynchronous distributed π-calculus named as routing calculi, 〖DR〗_π^(ω )and DRπ were the one of the significant developments towards modeling the distributed computer network using the router as an active component and considering the path of communication between the communicating nodes where a routing table is a dynamic entity in a typical distributed network. In formal modeling, the routing tables was updated upon creation of the new node in the network, but already existing entries in the routing table remain unchanged. We have done a comprehensive study of previous year's research in this area on the basis of which we derive our motivation with an intention to extend the existing routing calculi 〖DR〗_π^(ω ) to incorporate the dynamic updates of the routing table through the distance routing protocol. It has adaptive features based upon the network parameter changes. This model is closer to the real networks. These calculi are primarily considered as a metric to determine the quality of services (QoS).

Keyword

Routing calculi, Process calculi, π-calculus, Routing protocols.

Cite this article

Gupta P, Gaur M

Refference

[1][1]Milner R. Communication and concurrency. New York etc. Prentice hall; 1989.

[2][2]Hoare CA. Communicating sequential processes. In the origin of concurrent programming 1978 (pp. 413-43). Springer, New York, NY.

[3][3]Bergstra JA, Klop JW. Algebra of communicating processes with abstraction. Theoretical Computer Science. 1985; 37:77-121.

[4][4]Turner KJ, Van Sinderen M. LOTOS specification style for OSI. In LOTOSphere: software development with LOTOS 1995 (pp. 137-59). Springer, Boston, MA.

[5][5]Milner R. Communicating and mobile systems: the π-calculus. Cambridge University Press; 1999.

[6][6]Milner R, Parrow J, Walker D. A calculus of mobile processes, I. Information and Computation. 1992; 100(1):1-40.

[7][7]Milner R, Parrow J, Walker D. A calculus of mobile processes, II. Information and Computation. 1992; 100(1):41-77.

[8][8]Parrow J. An introduction to the π-calculus. In Handbook of Process Algebra 2001:479-543. Elsevier Science.

[9][9]Abadi M, Blanchet B, Fournet C. The applied pi calculus: mobile values, new names, and secure communication. Journal of the ACM (JACM). 2018; 65(1):1-41.

[10][10]Abadi M, Gordon AD. A calculus for cryptographic protocols: the spi calculus. Information and Computation. 1999; 148(1):1-70.

[11][11]Lanotte R, Merro M, Munteanu A. A modest security analysis of cyber-physical systems: a case study. In international conference on formal techniques for distributed objects, components, and systems 2018 (pp. 58-78). Springer, Cham.

[12][12]Avalle M, Pironti A, Sisto R. Formal verification of security protocol implementations: a survey. Formal Aspects of Computing. 2014; 26(1):99-123.

[13][13]Bowman H, Derrick J. Formal methods for distributed processing: a survey of object-oriented approaches. Cambridge University Press; 2001.

[14][14]Edric Fournet C, Gonthier G. The reflexive CHAM and the join-calculus. In proceedings of the POPL 1996 (pp. 372-85).

[15][15]Hennessy M. A distributed Pi-calculus. Cambridge University Press; 2007.

[16][16]Hennessy M, Gaur M. Counting the cost in the picalculus. Electronic Notes in Theoretical Computer Science. 2009; 229(3):117-29.

[17][17]Guar M. A routing calculus towards formalising the cost of computation in a distributed computer network (Doctoral dissertation, University of Sussex).2007.

[18][18]Gaur M. A routing calculus for distributed computing. In proceedings of doctoral symposium held in conjunction with formal methods 2008 (pp. 23-32).

[19][19]Guillemin F, Mazumdar R, Rosenberg C, Ying Y. Network calculus for mean delay analysis through a network. In international teletraffic congress 2018 (pp. 55-60). IEEE.

[20][20]Yadav P, Gaur M. A behavioural theory for intrusion detection system in mobile ad-hoc networks. In proceedings of the international conference on high performance compilation, computing and communications 2018 (pp. 51-60). ACM.

[21][21]De Nicola R, Ferrari G, Pugliese R, Tiezzi F. A formal approach to the engineering of domain-specific distributed systems. In international conference on coordination languages and models 2018 (pp. 110-41). Springer, Cham.

[22][22]Audrito G, Viroli M, Damiani F, Pianini D, Beal J. A higher-order calculus of computational fields. ACM Transactions on Computational Logic. 2019; 20(1).

[23][23]Xie W, Zhu H, Wu X, Vinh PC. Formal verification of mCWQ using extended hoare logic. Mobile Networks and Applications. 2019; 24(1):134-44.

[24][24]De Nicola R, Gorla D, Pugliese R. Basic observables for a calculus for global computing. Information and Computation. 2007; 205(10):1491-525.

[25][25]Griffin TG, Sobrinho JL. Metarouting. In ACM SIGCOMM computer communication review 2005 (pp. 1-12). ACM.

[26][26]Sewell P, Wojciechowski PT, Pierce BC. Location-independent communication for mobile agents: a two-level architecture. In international conference on computer languages 1998 (pp. 1-31). Springer, Berlin, Heidelberg.

[27][27]Francalanza A, Hennessy M. A theory of system behaviour in the presence of node and link failures. In international conference on concurrency theory 2005 (pp. 368-82). Springer, Berlin, Heidelberg.

[28][28]De Nicola R, Ferrari GL, Pugliese R. KLAIM: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering. 1998; 24(5):315-30.

[29][29]Montanari U, Sammartino M. Network-conscious π-calculus-a model of pastry. Electronic Notes in Theoretical Computer Science. 2015; 312:3-17.

[30][30]Gaur M, Kant R. A survey on process algebraic stochastic modelling of large distributed systems for its performance analysis. In international conference on eco-friendly computing and communication systems 2014 (pp. 206-11). IEEE.

[31][31]Gaur M, Gay SJ, Mackie I. A routing calculus with flooding updates. In international conference on distributed computing and internet technology 2015 (pp. 181-6). Springer, Cham.

[32][32]Sangiorgi D, Walker D. The pi-calculus: a theory of mobile processes. Cambridge University Press; 2003.

[33][33]Authentication I. Service for computer networks. IEEE Communications Magazine. 1994; 163.

[34][34]Cormen TH, Leiserson CE, Rivest RL, Stein C. Introduction to algorithms. MIT Press; 2009.

[35][35]Sobrinho JL. Network routing with path vector protocols: theory and applications. In proceedings of the conference on applications, technologies, architectures, and protocols for computer communications 2003 (pp. 49-60). ACM.

[36][36]Tang L, Liu Q. A survey on distance vector routing protocols. arXiv preprint arXiv:1111.1514.2011.

[37][37]Garcia-Luna-Aceves JJ. A unified approach to loop-free routing using distance vectors or link states. In ACM SIGCOMM computer communication review 1989 (pp. 212-23). ACM.

[38][38]Valadas R. OSPF and IS-IS: from link state routing principles to technologies. CRC Press; 2019.

[39][39]Gupta P, Gaur M. A routing calculus with distance vector routing updates. International Journal of Advanced Computer Science and Applications. 2018; 9(10):556-64.

[40][40]Sangiorgi D. A theory of bisimulation for the π-calculus. ACTA Informatica. 1996; 33(1):69-97.

[41][41]Pierce BC, Sangiorgi D. Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM (JACM). 2000; 47(3):531-84.

[42][42]Victor B, Moller F. The mobility workbench-a tool for the π-calculus. In international conference on computer aided verification 1994 (pp. 428-40). Springer, Berlin, Heidelberg.

[43][43]Bengtsson J, Larsen KG, Larsson F, Pettersson P, Yi W. UPPAAL in 1995. In international workshop on tools and algorithms for the construction and analysis of systems 1996 (pp. 431-4). Springer, Berlin, Heidelberg.

[44][44]DSouza KA, Khator SK. A survey of petri net applications in modeling controls for automated manufacturing systems. Computers in Industry. 1994; 24(1):5-16.