A New Verification Method Using Virtual System States for Responsive Communication Protocols and Its Application to a Broadcasting Protocol

摘要

Verification of responsive communication proto- cols is to determine whether they can recover to a normal state within a predetermined time, even when they enter an abnormal state due to any fault. In this paper, we propose a new verifica- tion method for responsive communication protocols using vir- tual system states, each of which represents several system states. Next, in order to evaluate the effectiveness of the new method, we develop a verification tool based on the proposed method. Then we apply the tool to a broadcasting protocol and measure several metrics on the tool. The experimental results show that (1) the number of system states, (2) the amount of memory used by the tool, and (3) the execution time of the tool, can be drastically reduced.