A Stochastic Extension of the Routing Calculi

The modern distributed systems have not only functional requirements (i.e. absence of deadlock, livelock etc.) but also have non-functional requirements (i.e. security, reliability, performance, Quality of Service(QoS) etc.). The methods for checking their correctness and analyze their performance is at very primitive stage. In the last few decades, formal verification techniques such as process algebras offer a powerful and rigorous approach for establishing the correctness of computer systems. Routing calculi (a such process algebra which is an elaboration of asynchronous distributed Pi calculus ) which models a distributed networks with router as an active component in determining the path between communicating processes. This algebra also take into account various types of routing tables updates upon creation of new nodes. The semantics of routing calculi has been defined to incorporate the cost of communicating processes after taking into consideration the number of routers crossings. In this paper, we survey to extend the routing calculi. This is done with an intention to aggregate the number of states in the state space of calculus. We propose this extension along the lines of PEPA nets. A brief sketch of the proposed extension is also given in this paper as future direction of our research. General Terms Pi Calculus, Formal Methods, PEPA nets, State Space Explosion