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 journalArticle

3 Citations (Scopus)

Abstract

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
Volume34
Issue number11
DOIs
Publication statusPublished - Oct 2003

Fingerprint

Satisfiability Problem
Communication Protocol
Finite automata
Specifications
Network protocols
State Transition
State Machine
Specification
Testing
Conformance Testing
Transition State
Configuration

Keywords

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

ASJC Scopus subject areas

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

Cite this

A Test Sequence Generation Method for Communication Protocols Using the SAT Algorithm. / Mori, Takanori; Otsuka, Hirotaka; Funabiki, Nobuo; Nakata, Akio; Higashino, Teruo.

In: Systems and Computers in Japan, Vol. 34, No. 11, 10.2003, p. 20-29.

Research output: Contribution to journalArticle

Mori, Takanori ; Otsuka, Hirotaka ; Funabiki, Nobuo ; Nakata, Akio ; Higashino, Teruo. / A Test Sequence Generation Method for Communication Protocols Using the SAT Algorithm. In: Systems and Computers in Japan. 2003 ; Vol. 34, No. 11. pp. 20-29.
@article{10d34bf4307b47c79199e325fb95a273,
title = "A Test Sequence Generation Method for Communication Protocols Using the SAT Algorithm",
abstract = "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.",
keywords = "Approximation algorithm, Communication protocol, Constraint, SAT algorithm, Test sequence generation problem",
author = "Takanori Mori and Hirotaka Otsuka and Nobuo Funabiki and Akio Nakata and Teruo Higashino",
year = "2003",
month = "10",
doi = "10.1002/scj.10482",
language = "English",
volume = "34",
pages = "20--29",
journal = "Systems and Computers in Japan",
issn = "0882-1666",
publisher = "John Wiley and Sons Inc.",
number = "11",

}

TY - JOUR

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

AU - Mori, Takanori

AU - Otsuka, Hirotaka

AU - Funabiki, Nobuo

AU - Nakata, Akio

AU - Higashino, Teruo

PY - 2003/10

Y1 - 2003/10

N2 - 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.

AB - 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.

KW - Approximation algorithm

KW - Communication protocol

KW - Constraint

KW - SAT algorithm

KW - Test sequence generation problem

UR - http://www.scopus.com/inward/record.url?scp=0141637321&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0141637321&partnerID=8YFLogxK

U2 - 10.1002/scj.10482

DO - 10.1002/scj.10482

M3 - Article

VL - 34

SP - 20

EP - 29

JO - Systems and Computers in Japan

JF - Systems and Computers in Japan

SN - 0882-1666

IS - 11

ER -