モデル検査を用いた通信プロトコル二重化の設計と検証(インターネットアーキテクチャ,一般,インターネットセキュリティ,一般)
スポンサーリンク
概要
- 論文の詳細を見る
高い信頼性を求めるサービスに対して高可用性を確保するためにフェイルオーバークラスタが利用されている.フェイルオーバー時にクラスタと通信相手が継続した通信を行うためにはプロトコルスタックの内部状態を同期する必要があるが,並行動作するマシンの数が増えるため,検証作業が困難になる問題がある.そこで,本研究ではクラスタの同期機構を設計段階で検証するために,SPINによるモデル検査を利用して通信プロトコル二重化の設計と検証を行った.
- 2009-06-11
著者
-
池田 聡
NECシステムプラットフォーム研究所
-
地引 昌弘
NECシステムプラットフォーム研究所
-
久野 靖
筑波大学大学院ビジネス科学研究科
-
西森 丈俊
筑波大学大学院ビジネス科学研究科
-
久野 靖
筑波大 大学院
-
久野 靖
筑波大学大学院
-
久野 靖
筑波大 大学院ビジネス科学研究科
関連論文
- モデル検査を用いた通信プロトコル二重化の検証(プロトコル,インターネット技術とその応用論文)
- モデル検査を用いた通信プロトコル二重化の設計と検証(インターネットアーキテクチャ,一般,インターネットセキュリティ,一般)
- Nuts : ホワイトボックスコンポーネントアーキテクチャ
- ベクターコンポーネント : コンポーネント結合による差分プログラミング
- Nuts-柔軟な部品間結合をサポートするコンポーネントアーキテクチャ
- 分散仮想マシンを用いたオブジェクト指向プログラミング環境
- アクションゲーム記述に特化した言語
- セッションスプライシングを用いたファイアウォール透過型VPNの評価(網・システム構築,情報通信マネジメント,一般)
- B-7-140 TCP Splicingを用いたFW透過型VPNにおけるTCP option整合方式(B-7. 情報ネットワーク,一般セッション)
- TCP無終端中継によるファイアウォール越え通信方式の検討(一般,インターネット、アプリケーション及び一般)
- B-6-43 TCPスプライシングを用いたファイアウォール越え通信の一検討(B-6.ネットワークシステム,一般講演)
- 1.情報科学教育の重要性と情報処理学会の活動(未来のコンピュータ好きを育てる)
- 中学校におけるCSアンプラグドの授業提案
- ペンコンピュータのUnix
- 「アイコン投げ」ユーザインタフェース ( インタラクティブソフトウェア)
- キーボードによる窓操作機構の作成と評価
- 中学校におけるコンピュータを使わない情報教育(アンプラグド)の評価
- プログラミング学習の他教科への波及効果(2) : 数学と考える力を対象とした調査と検証報告
- コンピュータサイエンスアンプラグドの状況と今後の展開
- 中学生が学会にやってきた
- 「新・試作教科書」におけるプログラミングの扱い(特別セッション 情報処理学会高校普通教科「情報」新・試作教科書)
- テレビゲーム記述プログラミング言語WOW
- K-025 視覚表現を用いたユーザー・オリエンテッドなシステム要求定義手法の提案 : ユーザー指向視覚的要求定義手法"すがた"の提案(K.ヒューマンコミュニケーション&インタラクション)
- WWWを環境を利用したビジネスゲーム開発ツール
- 「情報B」の教科書比較 : 「手順的な自動処理」の観点から
- モデル検査を用いた通信プロトコル二重化の検証
- モデル検査を用いた通信プロトコル二重化の設計と検証(インターネットアーキテクチャ,一般,インターネットセキュリティ,一般)
- 自然言語処理を用いた企業相関関係の取得
- 抽象状態同期による高機能ロックの実装と評価
- オブジェクト間の協調動作を表現する並列計算モデルと言語
- 対称型メッセージ送信とその実装
- パターン指向オブジェクト間協調計算モデルについて
- オブジェクト間協調動作表現モデルの提案 : 「プロデューサモデル」とその記述言語について
- 中学校における自律型制御ロボット教材の評価と授業〜新学習指導要領の「計測・制御」授業に向けて〜
- 自然言語処理を用いた企業相関関係の取得
- オーバレイネットワークにおけるスケーラブルなQoSルーティング方式(QoSとセキュリティ,ネットワーク制御,QoS,ルーティング,マルチキャスト及び一般)
- 近傍オブジェクトモデル(コンテンツネットワーク)(インターネットアーキテクチャ技術論文)
- 分散指向言語におけるオブジェクト外部情報の利用
- 分散オブジェクト指向言語の設計と実装
- オブジェクト指向言語とその発展 (特集 新しいコンピュータ言語環境)
- 「新・試作教科書」の全体構成と水準について(特別セッション 情報処理学会高校普通教科「情報」新・試作教科書)
- 2.情報教育におけるプログラミング利用の可能性(教育用プログラミング言語と授業利用)
- Join Tokens : オブジェクト間相互作用記述のための言語機構
- 美術教育での利用に適したプログラミング言語と環境
- 「教育用プログラミング言語に関するワークショップ2006」の報告
- 美術・工芸教育に適したプログラミング言語
- ドリトルと「情報教育の音楽化」
- 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高信頼通信方式の提案(インターネット及び一般)
- "Icon Throwing" user interface in tablet PC
- 教育用プログラミング言語におけるオブジェクト共有機能の導入
- 初中等教育におけるオブジェクト指向プログラミングの実践と評価
- オブジェクトストーム : オブジェクト指向言語による初中等プログラミング教育の提案(オブジェクト指向技術)
- 学校教育用オブジェクト指向言語「ドリトル」の設計と実装
- B-7-35 大規模無線センサNWにおける自律分散/自己組織的最短スパニングツリー構築手法および最適シンクノード位置決定手法(B-7.情報ネットワーク,一般セッション)
- ルータクラスタにおける二重パケット処理冗長方式(インターネット及び一般)
- ルータクラスタにおける二重パケット処理冗長方式(インターネット及び一般)
- プロトタイプ階層を持つ教育用オブジェクト指向言語「ドリトル」
- IPノード動的構成方式の提案(インターネット及び一般(2), インターネット及び一般)
- ルータクラスタにおける二重パケット処理冗長方式(アーキテクチャ, インターネットアーキテクチャ技術論文)
- B-6-146 二重パケット処理冗長クラスタの性能評価(B-6. ネットワークシステム, 通信2)
- コンピュータサイエンスアンプラグドに基づく授業方法改善の試みとその実践
- 特集「新しいアーキテクチャに基づくコンパイラ技術」の編集にあたって
- 監視制御システム用高信頼通信方式の試作(NWシステム)
- 高校情報科におけるネットワーク教育の内容と構成
- 言語研究者の「理想と現実」 (lt討論会gtさまざまなソフトウェア開発文明)
- 状態抽象 : モジュール化のもう1つの可能性
- 静的型検査を行なうオブジェクト指向言語Mistyにおける動的な型の扱い (オブジェクト指向研究会から)
- 新しいアーキテクチャとコンパイラ技術 (新しいアーキテクチャに基づくコンパイラ技術)
- 多重継承と強い型付けを持つオブジェクト指向言語Misty
- 4. 新しい技術の応用 4.1 新しいプログラマ・インタフェースの利用 (<大特集>新しいプログラミング環境)
- 確率的妥協に基づく契約関係が形成する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.楽しい学び実現?-高校生の意欲向上目指して-,大会企画シンポジウム,大会委員会企画)
- TK-7-5 高校教科「情報」におけるコミュニケーションの扱い(TK-7.楽しい学び実現?-高校生の意欲向上目指して-,大会企画シンポジウム,大会委員会企画)
- ランダム空間分割による位置情報データからの滞留点検出アルゴリズムの検討(モバイルユビキタス/センサ技術,アドホックネットワーク,RFID,一般及び技術展示)
- 初等中等教育における情報教育の過去・現在・未来