The combination of state transition model, axiomatic specification notations, and protocol is studied for logical deduction techniques of protocol analysis method as suggested by Sunshine. For axiomatic specification notions, axiomatic abstract data type that permits a representation-independent formal specification of a data type is applied to communication protocol specification.
The limitation of the Sunshine's methodology is analyzed, and the modified method is proposed for relaxation of limitation. As an example, a concurrent process model based on the data transfer functions of DoD's Transmission Control Protocol(TCP) is described and specified as the modified axiomatic abstract data type.
통신 Protocol들을 Formal하게 설계하고 검증하는 것이 최근에 점차적으로 중요시되고 있다. 여러 가지 Protocol의 해석 방법들이 사용되고 있는데, 크게 상태 공간 탐구법과 논리적 연역법으로 나누어 진다. 상태 공간 탐구법은 쉽게 기법화 될 수 있고 많은 실제적 방법에 사용되어 왔으나, 모델화 능력의 한계와 여러 성질들을 증명하는데 제한이 있다. 한편 논리적 연역법은 보다 강력한 기법이나, 사용하기 어렵고 지금까지 실용화에는 많은 어려움이 있었다.
본 논문에서는, Sunshine이 제시한, Protocol의 상태 변천 모형에 논리적 연역법의 적용을 위한 공리적 서술 개념에 대해서 알아보고, 한계점과 제한성을 분석하고 보완했다. 이런 공리적 서술을 위하여 Software 개발에서 중요한 개념으로 쓰이는 추상적 자료 형태를 통신 Protocol의 개발에 이용하는 것이다. 여기에서, 문제점 해결을 위하여 Sunshine의 기법에 개선된 방법을 제안하고, 미 국방성(DoD)의 Transmission Control Protocol을 기초로 한 전송 기능을 Concurrent Process Model로 하여 각각의 Module을 공리적 서술 방법인 개선된 추상적 자료 형태로 나타냄으로서 예로 삼았다.
