WEKO3
アイテム
SATアルゴリズムを利用したFSMプロトコルに対する試験系列生成の一手法
https://ipsj.ixsq.nii.ac.jp/records/88744
https://ipsj.ixsq.nii.ac.jp/records/88744360a6448-798e-43ca-8fb1-c17748e077c7
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 2002 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | Symposium(1) | |||||||
---|---|---|---|---|---|---|---|---|
公開日 | 2002-10-16 | |||||||
タイトル | ||||||||
タイトル | SATアルゴリズムを利用したFSMプロトコルに対する試験系列生成の一手法 | |||||||
タイトル | ||||||||
言語 | en | |||||||
タイトル | A Method to Generate Test Sequences for FSM Protocols using SAT Algorithm | |||||||
言語 | ||||||||
言語 | jpn | |||||||
資源タイプ | ||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
資源タイプ | conference paper | |||||||
著者所属 | ||||||||
大阪大学大学院基礎工学研究科 | ||||||||
著者所属 | ||||||||
岡山大学工学部 | ||||||||
著者所属 | ||||||||
大阪大学大学院情報科学研究科 | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Graduate School of Engineering Science, Osaka University | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Faculty of Engineering, Okayama University | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Graduate School of Information Science and Technology, Osaka University | ||||||||
著者名 |
森, 亮憲
船曵, 信生
東野, 輝夫
× 森, 亮憲 船曵, 信生 東野, 輝夫
|
|||||||
著者名(英) |
Takanori, Mori
Nobuo, Funabiki
Teruo, Higashino
× Takanori, Mori Nobuo, Funabiki Teruo, Higashino
|
|||||||
論文抄録 | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 本稿では,有限状態機械で記述された通信プロトコルに対して,SATを利用して状態確認を行うための試験系列を生成する手法を提案する.状態確認にはUIO系列を利用する.SATとは論理式の充足可能性を判定する問題である.提案手法では,論理式を用いて通信プロトコルの動作や試験系列が満たすべき条件を記述することから,各状態に対して複数のUIO系列が存在する場合や,UIO系列の重複を考慮した場合などに対応して試験系列を生成することができる.提案手法を実装し,DHCP(Dynamic Host Configuration Protocol)に適用して試験系列が生成できることを確認した. | |||||||
論文抄録(英) | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | In this paper, we propose a test sequence generation method for FSM protocols using SAT algorithm. UIO sequences are used for identifying states. SAT is a problem which check satisfiability of logical formulas. In our method, protocol behaviors and conditions which must be satisfied by test sequences are described as logical formulas. Hence our method can be applied to cases that each state has multiple UIO sequences and/or considering sequences overlapping. We developed a system, and apply it to DHCP (Dynamic Configuration Protocol) and generated test sequences. | |||||||
書誌情報 |
マルチメディア通信と分散処理ワークショップ論文集 巻 2002, 号 15, p. 75-80, 発行日 2002-10-16 |
|||||||
出版者 | ||||||||
言語 | ja | |||||||
出版者 | 情報処理学会 |