This dissertation presents a new technique to generate test sequence from a specification in System Description Language (SDL), in order to verify the conformity of the implementation with the specification.
In the generation of test sequences, concept of internal event and SIO(Set of Input Output) are introduced and an improved determinization algorithm is applied. From the state transition graph of the SDL specification, a global I/O FSM (Input/Output Finite State Machine) is obtained, it contains the external events having interactions with the SDL environment and the internal events being not visible from the SDL environment. A concept of the internal event allows to resolve the state space explosion. Afterwards, the global I/O FSM is transformed into a reference I/O FSM which is deterministic and minimal in accordance with the trace equivalence.
To resolve a possible problem of non-deterministic FSM into deterministic FSM, enhanced determination algorithm is applied. And UIO (Unique Input Output) sequences are used basically in the generation of test sequences. But for an identification sequence of the state without UIO sequence, the new concept of SIO is introduced to obtain a shorter length than the signature of the UIO method. Finally, to illustrate, the generation of optimized test sequences for the Inres protocol is presented.
본 논문은 프로토콜의 구현체가 규격과 일치하는 가를 검증하는 데 필요한 시험 계열을 시스템 기술 언어 (SDL : System Description Language)로 된 규격으로 부터 생성하는 새로운 기법을 제안한다.
시험 계열의 생성에 있어서는 internal (내부) 사건 및 SIO (Set of Input Output) 개념을 새로이 도입하였으며, 개선된 결정화 (Determinization) 알고리즘을 적용하였다. SDL 규격에 대한 시뮤레이션을 실시한 후에 얻어진 상태 변이 그래프로 부터 Global I/O FSM (Input/Output Finite Sate Machine)을 추출한다. 이 FSM은 PCO (Point of Control Observation)와 직접적인 상호 작용을 갖는 외부 사건과PCO에서는 보이지 않는 내부 사건들을 포함한다. 내부 사건의 개념은 상태 공간 팽창의 문제를 해결케 한다. 이후 Global I/O FSM 은 내부 사건을 축소시킨 Reference I/O FSM 으로 변환되며, 이 Reference I/O FSM은 trace equivalence에 따라 deterministic하며 minimal 한 특성을 갖는 FSM이다.
비결정적 FSM을 결정적 FSM으로 변환함에 있어서 제기되는 문제들을 해결하기 위하여 개선된 결정화 알고리즘을 적용하였다. 시험 계열을 생성함에 있어서는 기본적으로 UIO (Unique Input Output) 계열이 사용되었다. 그러나 UIO sequence를 갖지 않는 상태들에 대한 인식 계열의 생성에 있어서, UIO 방식의 Signature 보다 짧은 길이를 갖는 SIO(Set of Input Output)의 개념을 새로이 도입하였다.
본 방법의 적용 예로서 INRES 프로토콜에 대한 최적 시험 계열을 생성하였다.
