AUTOMATED VERIFICATION OF RESPONSIVE PROTOCOLS MODELED BY EXTENDED FINITE-STATE MACHINES

Along with advancement of communication systems, the demand for fault- tolerance and real-time performance for communication protocols contin ues to increase. Communication protocols which perform recovery from a ny abnormal state to a normal state are called self-stabilizing protoc ols. However, in these protocols, real-time recovery is not taken into consideration. This paper discusses verification of communication pro tocols which have self-stabilizing and timeliness properties, which ar e called responsive protocols. Gouda et al. proposed a mathematical me thod to prove whether a given protocol specification satisfies the sel f-stabilizing property. However, this method is not automated and does not verify the timeliness property. This paper thus proposes an autom ated method for verification of responsive protocols. In this method, communication protocols are modeled by extended finite state machines and their states are represented by predicates. The self-stabilizing p roperty is proven by verifying that sequences of such states which sta rt from an arbitrary abnormal state converge in a normal state. Also, the timeliness property is proven by verifying that the convergence is done within a priori given time.