Priyanka Gupta

Dynamic routing tables are pivotal in ensuring the efficiency and accuracy of large computational systems in both specification and implementation. These systems are subject to formal methods, which employ mathematical models for error-free development. The inherent mathematical functions in formal methods serve to validate the design, guaranteeing functionality, consistency, and reliability in the final product. The π-calculus stands out as a key calculus for modeling distributed systems, including the dynamic creation of names in forms such as DRπ and DRωπ. This proposed calculus can be regarded as an extension of the asynchronous distributed π-calculus, known as routing calculi DRπ and DRωπ. These developments played a crucial role in modeling distributed computer networks, emphasizing routers as active components and considering communication paths between nodes. In the existing models, routing tables remain fixed except when new nodes are added, leading to appended entries. The primary objective of implementing dynamic routing updates within these calculi was to establish a formal representation that closely resembles real-world networks. The proposed calculus aims to enhance Quality of Service (QoS) and subsequently boost performance by bridging the gap between formal modeling and actual distributed networks. Structured as a three-category syntactic expression, the proposed calculus envisions routers forming a non-clique undirected graph to facilitate connectivity. Nodes housing processes are directly linked to routers. Notably, the calculus introduces a unique aspect: periodic updates of routing tables through real-time exchanges among adjacent routers. This dynamic update mechanism ensures routers make optimal path choices during message propagation between communicating processes. Ultimately, the calculus asserts its proximity to real distributed networks within a process algebraic framework. When delving into the specifics, abstraction reveals that reduction equivalent up to structural equivalence are akin to a specification reminiscent of Dπ (distributed π-calculus). This assertion is substantiated by demonstrating that the proposed calculus can be validated through a touchstone equivalence between well formed configurations using reduction semantics. Furthermore, this equivalence can be mirrored through bi-simulation-based equivalence over labeled transition systems (LTS) and vice versa. By anchoring the discussion in the significance of dynamic routing tables, the proposed calculus emerges as an evolved extension of existing models, poised to bridge the gap between formalism and practical network functionality.