Simulation-Based Validation of Protocols for Distributed Systems

Protocol correctness in distributed systems means that a protocol achieves its intended goal without inducing any ill-effects on the application. The correctness issue becomes more important in Information Assurance applications where a protocol is designed to deal with hostile and unpredictable behavior of the processes and/or the network. The purpose of this paper is to provide a simulation-based methodology to validate the correctness of a candidate protocol. The methodology is based on state-machine modeling of the protocol in a context of its application-level goal and operating environment. The paper offers a 3-tier approach wherein a validation model captures the external constraints to be satisfied at the protocol interface, the environment perturbations the protocol is subjected to, and the protocol internal rules and procedures. Discrete-event simulators, developed in a suitable modeling language (such as PROMELA), check if a protocol meets the safety and liveness conditions prescribed at external interface to the protocol under a given operating environment. The modularity and designer-friendliness of our validation approach allow simulating di erent candidate protocols with ease and exibility. The paper illustrates our methodology with validation exercises on an alternating-bit data transfer protocol and a 2-phase commit based majority voting protocol.