프로토콜 명세의 검정과 적합성시험은 프로토콜 개발 과정에서 가장 중요한 부분으로, 명세에 규정되어진 시스템 기능의 정확성을 향상시키는데 사용되는 상호 보완 기술이다. 본 논문에서는 LTS(Labeled Transition System)로 명세화된 프로토콜 모델의 안전성 및 필연성 특성을 모형검사 기법에 의해 검정하였고, 실제적으로 교착상태의 유무나 초기 상태에서 임의의 상태로 도달 가능한지에 대한 검사를 실험적으로 증명하는 도구를 구현하였다. 구현된 프로토콜 검정기는 modal mu-calculus를 사용하여 modal 논리로 표현된 특성이 명세에 대해 올바른지 아닌지를 검정할 수 있다. 또한 검정되어진 프로토콜 명세로부터 UIO(Unique Input Output) 방법에 의해 유일한 입출력열을 이용하여 이끌어낸 결과 시퀀스가 구현에 대해 올바른지를 검사하는 적합성시험 계열 생성도구를 개발하였으며, 개발된 도구는 Windows NT 환경하에서 C++ 언어를 이용하여 구현되었다.
As a very important part in development of the protocol, verification and conformance test for protocol specification are complementary techniques that are used to increase the level of confidence in the system functions as prescribed by their specifications. In this paper, we verify the safety and liveness properties of rail signal control protocol type 1 specified in LTS with model checking method, and experimentally prove that it is possible to check for the deadlock, livelock and rechability of the states and actions on LTS. The implemented formal checker is able to verify whether properties expressed in modal logic are true in specifications using modal mu-calculus. We also propose a formal method on generation of conformance test cases using the concept of UIO sequences from verified protocol specification. The suggested tools are implemented by C++ language under Windows NT.
