Title :
A new decomposition method to relieve the state space explosion problem
Author :
Li, X. ; Lai, R. ; Dillon, T.S.
Author_Institution :
Dept. of Comput. Sci. & Comput. Eng., La Trobe Univ., Bundoora, Vic., Australia
Abstract :
Reachability analysis has proved to be one of most effective methods for protocol verification, but it is well known that it suffers from the state space explosion problem. In this paper, we present a new approach to generating state space in order to help relieve the state space explosion problem. In this approach, state space is generated and verified in stages. That is, only one subspace is involved in each stage of verification; upon completion, the memory occupied by a particular subspace can be released and subsequently used by the next subspace. The amount of memory needed for the verification of the whole protocol can be dramatically reduced, and thus the explosion problem relieved
Keywords :
conformance testing; formal verification; protocols; decomposition method; protocol verification; reachability analysis; state space explosion problem; Calculus; Computer science; Explosions; Protocols; Reachability analysis; Safety; State-space methods; System recovery;
Conference_Titel :
Computing and Information, 1993. Proceedings ICCI '93., Fifth International Conference on
Conference_Location :
Sudbury, Ont.
Print_ISBN :
0-8186-4212-2
DOI :
10.1109/ICCI.1993.315388