| 講演名 | 2009-06-19 モデル検査を用いた通信プロトコル二重化の設計と検証(インターネットアーキテクチャ,一般,インターネットセキュリティ,一般) 池田 聡, 地引 昌弘, 久野 靖, 西森 丈俊, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 高い信頼性を求めるサービスに対して高可用性を確保するためにフェイルオーバークラスタが利用されている.フェイルオーバー時にクラスタと通信相手が継続した通信を行うためにはプロトコルスタックの内部状態を同期する必要があるが,並行動作するマシンの数が増えるため,検証作業が困難になる問題がある.そこで,本研究ではクラスタの同期機構を設計段階で検証するために,SPINによるモデル検査を利用して通信プロトコル二重化の設計と検証を行った. |
| 抄録(英) | Fail-over clusters are utilized as a means to assure high-availability for services which require high reliability. If we need continuous communication during fail-over, it is required to synchronize internal states of a protocol stack of an active system and those of a stand-by system. It's, however, hard to verify the system because the number of machines which operate in parallel increases. In this paper, we have designed and verified some dual redundant communication protocols using the model checker SPIN for the purpose of a verifying synchronization mechanism at its design stage. |
| キーワード(和) | モデル検査 / 通信プロトコル / 冗長化 / TCP |
| キーワード(英) | model checking / communication protocol / redundancy / TCP |
| 資料番号 | IA2009-13,ICSS2009-21 |
| 発行日 |
| 研究会情報 | |
| 研究会 | ICSS |
|---|---|
| 開催期間 | 2009/6/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Information and Communication System Security (ICSS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モデル検査を用いた通信プロトコル二重化の設計と検証(インターネットアーキテクチャ,一般,インターネットセキュリティ,一般) |
| サブタイトル（和） | |
| タイトル（英） | Design and Verification of Dual Redundant Communication Protocols using Model Checking |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / model checking |
| キーワード(2)（和/英） | 通信プロトコル / communication protocol |
| キーワード(3)（和/英） | 冗長化 / redundancy |
| キーワード(4)（和/英） | TCP / TCP |
| 第 1 著者 氏名（和/英） | 池田 聡 / Satoshi IKEDA |
| 第 1 著者 所属（和/英） | NECシステムプラットフォーム研究所 System Platforms Research Laboratories, NEC Corporation |
| 第 2 著者 氏名（和/英） | 地引 昌弘 / Masahiro JIBIKI |
| 第 2 著者 所属（和/英） | NECシステムプラットフォーム研究所 System Platforms Research Laboratories, NEC Corporation |
| 第 3 著者 氏名（和/英） | 久野 靖 / Yasushi KUNO |
| 第 3 著者 所属（和/英） | 筑波大学大学院ビジネス科学研究科 Graduate School of Buisiness Sciences, University of Tsukuba |
| 第 4 著者 氏名（和/英） | 西森 丈俊 / Taketoshi NISHIMORI |
| 第 4 著者 所属（和/英） | 筑波大学大学院ビジネス科学研究科 Graduate School of Buisiness Sciences, University of Tsukuba |
| 発表年月日 | 2009-06-19 |
| 資料番号 | IA2009-13,ICSS2009-21 |
| 巻番号（vol） | vol.109 |
| 号番号（no） | 86 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |