Symbolic path-based protocol verification

Abstract

The principal problem in protocol verification is state explosion problem. In our work (W.C. Liu, C.G. Chung, Path-based Protocol Verification Approach, Technical Report, Department of Computer Science and Information Engineering, National Chiao-Tung University, Hsin-Chu, Taiwan, ROC, 1998), we have proposed a "divide and conquer" approach to alleviate this problem, the path-based approach. This approach-separates the protocol into a set of concurrent paths, each of which can be generated and verified independently of the others. However, reachability analysis is used to identify the concurrent paths from the Cartesian product of unit paths, and it is time-consuming. Therefore,:in this paper, we propose a simple and efficient checking algorithm-to identify the concurrent paths from the Cartesian product, using only Boolean and simple arithmetic operations. (C) 2000 Elsevier Science B.V; All rights reserved.