Finding Narrow Input/Output (NIO) Sequences by Model Checking

摘要

Conformance test sequences for communication protocols specified by finite state machines (FSM) often use unique input/output (UIO) sequences to detect state transition transfer faults. Since a UIO sequence may not exist for every state of an FSM, in the previous research, we extended UIO sequence to introduce a new concept called narrow input/output (NIO) sequence. The general computation of NIO sequences may lead to state explosion when an FSM is very large. In this paper, we present an approach to find NIO sequences using symbolic model checking. Constructing a Kripke structure and a computation tree logic (CTL) formula for such a purpose is described in detail. We also illustrate the method using a model checker SMV.