The network topology of a communication system is often represented by a directed labeled graph in which there exists one and only one elementary path from one node to any other node. Nodes and arcs in this graph represent the processes in the communication system and the links between the processes, respectively. In this thesis, we propose an algorithm for validation of the protocols in the restricted class of communication systems with such a network topology. For this algorithm, protocols are represented by N(N≫2) communicating finite state machines. The algorithm can detect deadlocks and unspecified receptions with savings in computation time and/or storage space in comparison with the conventional perturbation technique.
컴퓨터 네트워크의 발달로 인하여 통신 프로토콜의 개발및 표준화에 대한 연구가 활발히 수행되고 있으며, 이에따라 통신 프로토콜의 작성(specification) 및 검증(validation) 기법도 다양화되고 있다. 본 논문에서는 가장 보편적으로 사용되고 있는 프로토콜 검증 기법인 퍼터베이션 기법(perturbation technique)의 효율(efficiency)을 높이기 위하여 새로운 state exploration 방법을 개발하였으며 이 방법에 기초를 둔 효율적인 프로토콜 검증 기법을 제시하였다.
본 논문에서 개발된 state exploration 방법은 제한된 프로토콜에만 적용될 수 있으나, 그 적용 범위가 두 개의 finite state machine으로 구성된 프로토콜에만 국한되지 않으므로 퍼터베이션 기법의 효율을 높이기 위하여 제시되었던 다른 어떤 state exploration 방법들 보다 그 적용 범위가 넓다.
본 논문에서 제시된 프로토콜 검증 기법을 X.25및 X.21등 실제로 사용되고 있는 프로토콜을 비롯한 4종류의 프로토콜에 적용하여 제시된 프로토콜 검증 기법이 퍼터베이션 기법에 비하여 효율적임을 실험적으로 증명하였으며, 두 가지 검증기법이 생성하는 state 수 들의 maximal bound를 channel capacity및 finite state machine 내의 node수로 표시하여 그 효율을 상대적으로 비교하였다.
