モデル検査を用いた通信プロトコル二重化の検証(プロトコル,<特集>インターネット技術とその応用論文)
スポンサーリンク
概要
- 論文の詳細を見る
高い信頼性を求めるサービスに対して高可用性を確保するために,フェイルオーバクラスタが利用されている.このようなシステムでは,フェイルオーバ時にクラスタと通信相手が継続した通信を行うために,プロトコルスタックの内部状態を同期する必要がある.しかし,並行動作するマシンの数が増えると,同期機構の検証作業が困難になるという問題が生じる.そこで,本論文ではクラスタの同期機構を設計段階で検証するため,モデル検査を利用した通信プロトコル二重化の検証手法を提案する.提案手法では,モデル検査を用いることにより,設計段階における不具合の早期発見が可能である.加えて,単体システムのモデルとその形式仕様をクラスタの検証に活用することにより,通信プロトコル二重化の検証を汎用的な手順で行うことができる.提案手法をTCPの二重化に対して適用し,提案手法の有効性を確認した.
- 2010-07-01
著者
-
池田 聡
NECシステムプラットフォーム研究所
-
地引 昌弘
NECシステムプラットフォーム研究所
-
久野 靖
筑波大学大学院ビジネス科学研究科
-
西森 丈俊
筑波大学大学院ビジネス科学研究科
-
久野 靖
東京工業大学理学部情報科学科
-
久野 靖
筑波大 大学院
-
久野 靖
筑波大学
-
久野 靖
東京工業大学理学部
-
久野 靖
筑波大学大学院
-
久野 靖河
東京工業大学理学部情報科学科
-
久野 靖
筑波大 大学院ビジネス科学研究科
関連論文
- モデル検査を用いた通信プロトコル二重化の検証(プロトコル,インターネット技術とその応用論文)
- ITクラフトマンシッププロジェクト : 小中学生によるドリトルプログラミング
- モデル検査を用いた通信プロトコル二重化の設計と検証(インターネットアーキテクチャ,一般,インターネットセキュリティ,一般)
- Nuts : ホワイトボックスコンポーネントアーキテクチャ
- ベクターコンポーネント : コンポーネント結合による差分プログラミング
- Nuts-柔軟な部品間結合をサポートするコンポーネントアーキテクチャ
- 分散仮想マシンを用いたオブジェクト指向プログラミング環境
- アクションゲーム記述に特化した言語
- セッションスプライシングを用いたファイアウォール透過型VPNの評価(網・システム構築,情報通信マネジメント,一般)
- B-7-140 TCP Splicingを用いたFW透過型VPNにおけるTCP option整合方式(B-7. 情報ネットワーク,一般セッション)
- TCP無終端中継によるファイアウォール越え通信方式の検討(一般,インターネット、アプリケーション及び一般)
- B-6-43 TCPスプライシングを用いたファイアウォール越え通信の一検討(B-6.ネットワークシステム,一般講演)
- 1.情報科学教育の重要性と情報処理学会の活動(未来のコンピュータ好きを育てる)
- 中学校におけるCSアンプラグドの授業提案
- CLUマシンシステムの開発
- ペンコンピュータのUnix
- 「アイコン投げ」ユーザインタフェース ( インタラクティブソフトウェア)
- 中学校におけるコンピュータを使わない情報教育(アンプラグド)の評価
- プログラミング学習の他教科への波及効果(2) : 数学と考える力を対象とした調査と検証報告
- コンピュータサイエンスアンプラグドの状況と今後の展開
- 中学生が学会にやってきた
- 「新・試作教科書」におけるプログラミングの扱い(特別セッション 情報処理学会高校普通教科「情報」新・試作教科書)
- テレビゲーム記述プログラミング言語WOW
- K-025 視覚表現を用いたユーザー・オリエンテッドなシステム要求定義手法の提案 : ユーザー指向視覚的要求定義手法"すがた"の提案(K.ヒューマンコミュニケーション&インタラクション)
- WWWを環境を利用したビジネスゲーム開発ツール
- 「情報B」の教科書比較 : 「手順的な自動処理」の観点から
- モデル検査を用いた通信プロトコル二重化の検証
- モデル検査を用いた通信プロトコル二重化の設計と検証(インターネットアーキテクチャ,一般,インターネットセキュリティ,一般)
- スクリプト言語(1)座談会「スクリプト言語とは」
- 自然言語処理を用いた企業相関関係の取得
- 抽象状態同期による高機能ロックの実装と評価
- オブジェクト間の協調動作を表現する並列計算モデルと言語
- 対称型メッセージ送信とその実装
- パターン指向オブジェクト間協調計算モデルについて
- オブジェクト間協調動作表現モデルの提案 : 「プロデューサモデル」とその記述言語について
- 大特集「オブジェクト指向プログラミング」の編集にあたって
- 中学校における自律型制御ロボット教材の評価と授業〜新学習指導要領の「計測・制御」授業に向けて〜
- 自然言語処理を用いた企業相関関係の取得
- オーバレイネットワークにおけるスケーラブルなQoSルーティング方式(QoSとセキュリティ,ネットワーク制御,QoS,ルーティング,マルチキャスト及び一般)
- 近傍オブジェクトモデル(コンテンツネットワーク)(インターネットアーキテクチャ技術論文)
- 分散指向言語におけるオブジェクト外部情報の利用
- 分散オブジェクト指向言語の設計と実装
- オブジェクト指向言語とその発展 (特集 新しいコンピュータ言語環境)
- 「新・試作教科書」の全体構成と水準について(特別セッション 情報処理学会高校普通教科「情報」新・試作教科書)
- 2.情報教育におけるプログラミング利用の可能性(教育用プログラミング言語と授業利用)
- Join Tokens : オブジェクト間相互作用記述のための言語機構
- 美術教育での利用に適したプログラミング言語と環境
- 「教育用プログラミング言語に関するワークショップ2006」の報告
- ITクラフトマンシッププロジェクト : 中学生によるネットワークプログラミング
- 美術・工芸教育に適したプログラミング言語
- ドリトルと「情報教育の音楽化」
- B-6-66 契約関係においてコンセンサスと妥協が生成するNW(B-6.ネットワークシステム,一般セッション)
- システム運用時に発生する障害の再発防止策の適用方法に関する提案
- ペンコンピュータのUnix
- トラヒック短期変動の影響を考慮した利用可能帯域測定方式(五感メディア,映像/音声サービスの品質,ワイヤレスネットワークの品質,次世代ネットワークアーキテクチャ,一般)
- B-7-47 トラヒック短期変動を推定可能な利用可能帯域計測方式(B-7.情報ネットワーク,一般講演)
- B-6-5 オーバレイネットワークにおける効率的な仮想リンク品質計測方式(B-6.ネットワークシステム,一般講演)
- 無線マルチホップネットワークにおけるアプリケーション適応型メトリックを用いたリアクティブ型経路制御方式(インターネット技術及び一般II)
- トランスポート端点のポータブルなクラスタ方式(インターネット技術及び一般I)
- 無線マルチホップネットワークにおけるアプリケーション適応型メトリックを用いたリアクティブ型経路制御方式(インターネット技術及び一般II)
- トランスポート端点のポータブルなクラスタ方式(インターネット技術及び一般I)
- 不安定なリンクを考慮したマルチパス高信頼通信方式の提案(ブロードバンドユビキタスネットワーク時代におけるインターネットアーキテクチャ論文)
- IPノード動的構成方式の提案(インターネット及び一般(2), インターネット及び一般)
- システム開発外部委託管理のためのプロセス標準化(「ビジネスモデルからソーシャルモデルへの展開」 : 企業から公共,非営利組織まで)
- 「新・試作教科書」における情報社会/情報倫理の扱い(特別セッション 情報処理学会高校普通教科「情報」新・試作教科書)
- 5X-7 情報教育のためのソフトウェア環境への要件 : 計算機科学との連携
- スレッドライブラリへの抽象状態同期の導入
- 抽象状態に基づく並列オブジェクト指向言語p6
- NetNewsサーバにおける効率的な記事配送方式の設計と実装
- 無線マルチホップネットワークにおけるMPLS高信頼通信方式の提案(インターネット及び一般)
- 無線マルチホップネットワークにおけるMPLS高信頼通信方式の提案(インターネット及び一般)
- 新しい情報教育環境 (特集 初等中等教育に広がる情報教育)
- 高校教科「情報」のこれまでとこれから(前) (ぺた語義(第1回))
- 並列オブジェクト指向言語を用いたTMSの再構成
- データ抽象向けプログラム設計技法
- 教育用プログラミング言語におけるオブジェクト共有機能の導入
- 初中等教育におけるオブジェクト指向プログラミングの実践と評価
- オブジェクトストーム : オブジェクト指向言語による初中等プログラミング教育の提案(オブジェクト指向技術)
- 学校教育用オブジェクト指向言語「ドリトル」の設計と実装
- B-7-35 大規模無線センサNWにおける自律分散/自己組織的最短スパニングツリー構築手法および最適シンクノード位置決定手法(B-7.情報ネットワーク,一般セッション)
- ルータクラスタにおける二重パケット処理冗長方式(インターネット及び一般)
- ルータクラスタにおける二重パケット処理冗長方式(インターネット及び一般)
- プロトタイプ階層を持つ教育用オブジェクト指向言語「ドリトル」
- IPノード動的構成方式の提案(インターネット及び一般(2), インターネット及び一般)
- ルータクラスタにおける二重パケット処理冗長方式(アーキテクチャ, インターネットアーキテクチャ技術論文)
- B-6-146 二重パケット処理冗長クラスタの性能評価(B-6. ネットワークシステム, 通信2)
- 高校教科「情報」のこれまでとこれから(後) (ぺた語義(第2回))
- プログラミング言語(に関する用語集) (特集 新人技術者・研究者に捧ぐ) -- (第1部 技術知識編)
- 型階層をもつオブジェクト指向言語 (オブジェクト指向プログラミング)
- 監視制御システム用高信頼通信方式の試作(NWシステム)
- 確率的妥協に基づく契約関係が形成するNWトポロジの解析(一般,高度プロトコル・ネットワーキング技術(IP及び高位レイヤルーチング・フィルタリング,マルチキャスト,品質・経路制御,IPNWの利用技術(P2P,P4P,オーバレイ,SIP,NGN),ネットワークシステム関連技術(システム構成法,インタフェース,アーキテクチャ,ハードウェア・ソフトウェア・ミドルウェア),一般)
- 大規模無線センサNWにおける自律分散/自己組織的最短スパニング・ツリー構築手法および最適シンクノード位置決定手法(一般,高度プロトコル・ネットワーキング技術(IP及び高位レイヤルーチング・フィルタリング,マルチキャスト,品質・経路制御,IPNWの利用技術(P2P,P4P,オーバレイ,SIP,NGN),ネットワークシステム関連技術(システム構成法,インタフェース,アーキテクチャ,ハードウェア・ソフトウェア・ミドルウェア),一般)
- B-19-46 LSHを用いた空間分割による滞留点推定の理論的考察(B-19. ユビキタス・センサネットワーク,一般セッション)
- Random Space Partitioning for extracting significant locations from GPS data (ユビキタス・センサネットワーク)
- TK-7-5 高校教科「情報」におけるコミュニケーションの扱い(TK-7.楽しい学び実現?-高校生の意欲向上目指して-,大会企画シンポジウム,大会委員会企画)
- TK-7-5 高校教科「情報」におけるコミュニケーションの扱い(TK-7.楽しい学び実現?-高校生の意欲向上目指して-,大会企画シンポジウム,大会委員会企画)
- TK-7-5 高校教科「情報」におけるコミュニケーションの扱い(TK-7.楽しい学び実現?-高校生の意欲向上目指して-,大会企画シンポジウム,大会委員会企画)
- TK-7-5 高校教科「情報」におけるコミュニケーションの扱い(TK-7.楽しい学び実現?-高校生の意欲向上目指して-,大会企画シンポジウム,大会委員会企画)
- ランダム空間分割による位置情報データからの滞留点検出アルゴリズムの検討(モバイルユビキタス/センサ技術,アドホックネットワーク,RFID,一般及び技術展示)
- 初等中等教育における情報教育の過去・現在・未来