In this thesis, to improve the efficiency of state exploration and to solve (or relieve) the problem of state explosion, we propose another method of state exploration called the extended circular exploration (ECE), which does not need to explore all the reachable global states and can be applied to N-party protocol with alternative routes, i.e., it is applicable to the protocol in which adaptive routing mechanism can be performed. Using this ECE, we can eliminate the topology restriction of the CE through extending the notions of circular exploration. That is to say, in this thesis, we explore only those global states which are reachable, provided that the participant processes of any group of transitions proceed at the same speed, and that they can be formed as a cycle. The state space thus explored is not exhaustive.
The algorithm presented can detect deadlock error and unspecified reception error. It requires stotage space and/or execution time much less than those of the CP but, a little more than those of Hwang's technique. However the results of validation are more correct than those of Hwang's with this generalized network topology. It can be viewed as a solution of the N-process collision and the interference mechanism [Rubi82].
본 논문에서는 프로토콜 검증 방법의 하나인 도달 분석 (reachability analysis)의 문제였던 상태 폭발 (state explosion)의 문제를 해결하고, 상태 탐색 (state exploration)의 효율성을 개선하기 위해 확장된 원형 탐색이라 불리우는 새로운 상태 탐색 방법을 제시하였다. 이 방법은 도달 가능한 모든 전체 상태를 탐색하는 대신에, 상태 천이에 참여한 프로세스 들이 싸이클(cycle)을 형성하고 그 내부에서는 모든 프로세스 들이 동일한 속도로 전진해서 도달 할 수 있는 상태만을 탐색 한다. 이렇게 탐색된 상태들은 기존의 그 것보다 현저히 적어서 상태 폭발을 야기 하지 않는다. 또 이 방법이 대체 경로를 갖고 있는 N-파티 프로토콜에 적용 될 수 있도록 원형 그룹의 개념을 확장 하여 기존 방법의 제한을 제거하였다.
이 방법은 데드 락 (deadlock error)과 언급 안 된 수신 (unspecified reception error) 에러를 검출 할 수 있으며, 그 과정에 소요 되는 상태 공간 (state space)과 수행시간 (excution time)은 기존의 그 것 들 보다 현저히 적다.
