In this thesis, an efficient protocol verification system named LOVE has been designed and implemented. LOVE has been developed specifically for LOTOS(language for temporal ordering specification) which has been developed as a Formal Description Technique by ISO(International Standard Organization) for the description of the OSI(Open System Interconnection) architecture.
Protocol verification in LOVE is done in two steps, protocol syntax validation(PSV) and protocol functional verification(PFV). PSV is a test to check if a protocol is free from protocol syntax errors such as deadlocks, unspecified receptions, state ambiguities and livelocks. PFV confirms whether a protocol achieves its functional objectives. The reachability analysis is done for the PSV and the observational equivalence test is used for the PFV.
LOVE, an abbreviation for LOtos VErifier, is the name given to a set of programs and command files which can be used for protocol simulation, PSV, and PFV. The input domain of the LOVE is a subset of LOTOS called the basic LOTOS. The basic LOTOS is an abridged version of the language employing a finite set of observable actions. The basic LOTOS deals with gate synchronization, but it does not check passing data values. LOVE has been installed on a SUN 3/280 machine running under the Unix operating system(OS), but it can be installed on any other Unix OS systems because it has no hardware-dependent codes. All programs have been written in C language.
LOVE has two main parts, action tree builder(ATB) and equivalence tester(ET). The first main part, ATB, executes a basic LOTOS specification in batch mode, generates the corresponding action tree, and performs the PSV. Action tree is a kind of labelled transition diagram in which state information is contained implicitly. Because LOTOS is an event-based FDT, an action tree contains all dynamic characteristics of the LOTOS specification. The reachability analysis is performed on an action tree of the PSV. The second main part of LOVE, ET, is a PFV tool based on the observational equivalence of two action trees. It verifies that a formally described system specification behaves equivalently to an assigned, possibly more abstract system specification.
For the protocol verification using LOVE, a schematic protocol verification methodology has been outlined. Using the methodology, the alternating bit protocol(ABP), which may be regarded as a typical example in the test of different FDT techniques and protocol verifications has been specified and verified to test the ability of LOVE.
A major contribution of this thesis is that it has for the first time performed a PSV on the protocol specifications based on the event-based FDT. The most important role of LOVE is to perform PFV. The PFV presupposes a clear definition of the properties to be verified. Many current protocols are so complex that it is difficult to define a general method for PFV. Because LOTOS is a behavioral FDT, the PFV can be achieved by the behavioral equivalence test in the LOVE. As the ESPRIT/SEDOS LOTOS toolset has been developed in C language under the Unix OS like LOVE, LOVE should be very useful to set up an integrated protocol development tools based on LOTOS.
본 논문에서는 LOVE라 불리는 프로토콜 검증 시스템을 개발하였다. 일반적으로 프로토콜 검증 방법은 프로토콜 표현기법에 의해 많이 좌우되는데 LOVE 시스템은 프로토콜 표현기법으로, 국제표준화기구에서 분산시스템 및 프로토콜 개발을 위한 형식언어를 목표로 1988년도에 국제표준화한 LOTOS의 사용을 전제로 하였다.
LOVE 시스템을 이용한 프로토콜 검증은 프로토콜의 일반적 특성 검사와 프로토콜의 고유 기능 검사의 두개의 과정으로 나누어 수행된다. 프로토콜의 일반적 특성 검사란 모든 프로토콜이 공통적으로 지니는 특성을 검사하는 것으로, 설계된 프로토콜이 deadlock, unspecified reception, state ambiguity, livelock 등의 에러를 포함하고 있지 않은가를 조사하는 것이다. 프로토콜의 고유 기능 검사는 목표로 하는 프로토콜 서비스와, 프로토콜 개발자가 실제로 설계한 프로토콜이 그 기능상에서 일치하는 지를 보이는 것이다. LOVE 시스템에서는 프로토콜의 일반적 특성 검사를 위해서는 reachability analysis를 사용하였고 프로토콜의 고유 기능 검사를 위해서는 observational equivalence 관계를 이용하였다.
LOVE는 LOtos VErifier의 약자로, LOTOS를 표현 언어로 사용하여 프로토콜을 개발할 경우 설계단계에서 그 프로토콜 잘못된 점의 존재 여부를 알려주는 프로그램이다. LOVE 시스템은 Unix 운영체제하의 SUN 3/280 시스템상에서 개발되었으며 전부 C 프로그래밍 언어로 작성되었으므로 Unix 운영체제하의 어느 시스템에서도 바로 사용될 수 있다. LOVE 시스템은 크게 두개의 소프트웨어 tool로 구성되는데 action tree builder(ATB)와 equivalence tester(ET)가 그것이다. 첫번째 tool인 ATB는 LOTOS로 표현된 프로토콜을 수행시켜 action tree를 얻는데, action tree란 그 프로토콜 프로세스가 다른 모든 프로세스와 메시지를 주고받는 모든 순서를 표현한 상태천이도이다. 따라서 action tree는 프로토콜의 동적특성을 나타내는 모든 정보를 포함한다. ATB는 이 action tree 에 reachability analysis를 이용함으로써 프로토콜의 deadlock, livelock 등 프로토콜의 일반적 특성 검사를 수행한다. 두번째 tool인 ET는 프로토콜의 고유 기능 검사를 수행하는 것으로 그 과정은 서비스와 프로토콜을 각각 LOTOS로 표현한 뒤, 이들에 대해 ATB를 수행시켜 그 결과로 얻어진 두개의 action tree에 대한 observational equivalence를 조사해 봄으로써 이루어진다.
본 논문에서는 LOVE를 사용하여 프로토콜 검증을 수행하기 위한 체계적인 프로토콜 검증 방법론을 제시했으며, 여러 논문에서 프로토콜 검증 이론 및 tool을 비교 분석하는데 있어서 전형적인 예로 보여 졌던 alternating bit protocol을 가지고 LOVE 시스템의 유용성을 검사하였다.
본 논문이 기여한 점은 첫째로 LOTOS와 같은 event-based 표현 언어로 표현된 프로토콜에 대해 처음으로 reachability analysis를 이용하여 프로토콜의 일반적 특성 검사를 수행했다는 점이며, 둘째로 여태까지 다른 논문에서 별로 진행되지 못했던 프로토콜의 고유 기능 검사를 실제로 수행함으로써 프로토콜의 검증이 프로토콜 전 개발과정에 있어 얼마나 유용하게 사용되는지를 보였다는 것이다. 셋째로 LOVE 시스템은, ESPRIT/SEDOS 프로젝트에서 개발한 LIW(LOTOS Implementation Workbench)와 같이 UNIX 운영체제하에서 C 프로그래밍 언어를 사용해 개발되었으므로 이들과 함께 LOTOS를 기반으로 하는 종합적인 프로토콜 개발시스템을 구성하는데 기여할 수 있다는 점이다.
LOTOS는 Milner의 CCS(Calculus of Communication Systems) 이론에 기본을 둔 프로세스 표현부와 프로그래밍언어 ACT ONE의 abstract data type 이론에 기본을 둔 데이타 표현부로 구성된다. 현재 LOVE 시스템은 프로세스간의 동기화, 즉 프로세스 표현부만을 다루는 basic LOTOS를 표현 언어로 사용하는 경우에 대해서만 검증을 수행하고 있다. 데이타 표현부가 포함된 완전한 LOTOS를 표현 언어로 사용할 경우 이에 대한 검증 시스템의 개발은 앞으로 더 연구해야 할 문제이다.
