In this thesis, the state transition model of protocol and validation of its syntactic properties such as deadlock-freeness, well-formedness, and channel boundedness are discussed with the reachability analysis of the Petri-net.
The tool for the automatic validation of any given two-process protocol model with non-FIFO channels and reception maskable states is also developed. By using this tool implemented in C language, the connection establishment protocol in Transmission Control Protocol(TCP) is validated. The result is that state deadlocks and channel overflows are not found but unspecified receptions which are recoverable semantically are found.
Finally, the validation considering reception maskable states is shown to be more efficient than the validation not considering these states.
프로토콜이 제 기능을 발휘하는지를 보증하기 위하여 여러가지 검증 방법들이 연구되어왔다.
본 논문에서는 프로토콜의 상태 천이 모형화 및 그의 구문법적인 (syntactic) 특성들 즉 deadlock-freeness, well-formedness, 및 channel상 메세지의 유한성들의 검증 방법에 관하 여 고찰하였으며, 이때 Petri-net에 있어서의 reachability 분석 방법이 이론적으로 도입되었다.
또한 임의의 두 프로세스간에 FIFO 특성을 갖지 않는 channel 을 가정하고 각 프로세스가 메세지 수신을 무시할수 있는(reception maskable) 상태를 가정한 프로토콜 모형의 구문법적인 특성을 자동적으로 검증할 수 있도록 하는 도구(tool)가 C language를 이용하여 구현되었다. 이를 이용하여 TCP 내의 접속 형성(connection establishment) 프로토콜이 검증되었다. 그 결과 state deadlock과 channel overflow 오류가 검출되지 않았으며 의미론 적으로(semantically) 보상될 수 있는 unspecified reception 현상이 발생할 수 있음을 알아냈다.
끝으로 메세지 수신을 무시할 수 있는 상태들을 가정했을 경우의 검증 결과가 그러한 상태들을 가정하지 않았을 경우 보다 더 효율적 임을 예를 들어서 보였다.
