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

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

Research output: Contribution to journalArticlepeer-review

3 Citations (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.

Original languageEnglish
Pages (from-to)20-29
Number of pages10
JournalSystems and Computers in Japan
Issue number11
Publication statusPublished - Oct 2003


  • Approximation algorithm
  • Communication protocol
  • Constraint
  • SAT algorithm
  • Test sequence generation problem

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Hardware and Architecture
  • Computational Theory and Mathematics


Dive into the research topics of 'A Test Sequence Generation Method for Communication Protocols Using the SAT Algorithm'. Together they form a unique fingerprint.

Cite this