Simulation-based validation of protocols for concurrent systems

Protocol correctness in multi-process concurrent 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 different candidate protocols with ease and flexibility. The paper illustrates our methodology with validation exercises on a 2-phase commit based majority voting protocol.