A Test Sequence Generation Method for Communication Protocols Using the SAT Algorithm

Takanori Mori, Hirotaka Otsuka, Nobuo Funabiki, Akio Nakata, Teruo Higashino


3 被引用数 (Scopus)


The specification for a communication protocol is generally represented by a finite-state machine, and the operation of the machine is represented by transitions among states. The device implementing such specification is called the implementation under test (IUT). It is important for the IUT that its operation should be verified for all state transitions on the finite-state machine given in the specification. This test is called the conformance testing. In such testing it is important to generate efficiently a route containing all state transitions from the initial state. This problem is called the test sequence generation problem. This paper considers the test sequence generation problem for a communication protocol and proposes an application of an algorithm for satisfiability problem (SAT) that can flexibly handle various constraints, such as the order constraint and the time constraint among multiple constraints. The proposed method is applied to the dynamic host configuration protocol (DHCP) and its effectiveness is demonstrated.

ジャーナルSystems and Computers in Japan
出版ステータスPublished - 10月 2003

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • 情報システム
  • ハードウェアとアーキテクチャ
  • 計算理論と計算数学


「A Test Sequence Generation Method for Communication Protocols Using the SAT Algorithm」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。