Title :
Finding Narrow Input/Output (NIO) Sequences by Model Checking
Author :
Huang, Tao ; Chung, Anthony
Author_Institution :
Sch. of Comput. Sci. Telecommun. & Inf. Syst., DePaul Univ. Chicago, Chicago, IL
Abstract :
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.
Keywords :
conformance testing; finite state machines; formal logic; formal verification; protocols; support vector machines; trees (mathematics); Kripke structure; SMV model checker; communication protocols; computation tree logic formula; conformance test sequences; finite state machines; model checking; narrow input/utput sequences; state transition transfer faults; symbolic model checking; unique input/output sequences; Automata; Conference management; Engineering management; Explosions; Fault detection; Logic; Protocols; Software engineering; Tail; Testing; Communication protoocls; model checking; protocol engineering; protocol testing;
Conference_Titel :
Software Engineering Research, Management and Applications, 2008. SERA '08. Sixth International Conference on
Conference_Location :
Prague
Print_ISBN :
978-0-7695-3302-5
DOI :
10.1109/SERA.2008.42
