Simulation and probabilistic validation of communication protocols

Protocol Validation is the process of showing that a (suitably specified) protocol has certain (suitably specified) properties, for example, that it is free from deadlocks. In the past, the acceptance of automated tools for the validation of protocols has been hindered by three main problems: (1) most validation tools are lacking in the level of realism they support: they are either unable to deal with the timing aspects (e.g., delays between events) or the probabilistic aspects (e.g., probability of loss) of protocols; (2) unlike most performance evaluation tools which are based on common programming languages like C or C++, validation tools often employ special-purpose languages (e.g., PROMELA in S PIN, KRONOS); and (3) protocol validation is computationally difficult due to the state space explosion problem—the fact that the state space of a protocol is exponential in the number of variables and processes. Validation algorithms published in the literature often have unrealistic resource requirements.; In this thesis, we propose a validation tool that addresses these problems. Our tool is based on the well-known discrete event simulation (DES) paradigm and checks whether a property expressed in a simple linear-time logic (event logic, (EL)) is satisfied by a protocol. The tool is based on DES and thus supports time and probabilities (problem 1 above). Problem (2) is addressed by implementing the tool as a C++ library. To better deal with the state explosion problem, we propose using state transition probabilities as a heuristic to guide the state space search, and present some memory-efficient algorithms for the checking of EL formulas. An added advantage of our approach is that the same protocol specification can be used for both performance evaluation by simulation and for validation. A number of experiments described in the thesis demonstrate the feasibility of our validation tool.