Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出(ソフトウェアシステム)
スポンサーリンク
概要
- 論文の詳細を見る
Hadoop MapReduceはデータとしてキーと値による組を利用する大規模並列処理を行うためのフレームワークであり,今日では広く利用されている.目的の処理を行うため,Map及びReduce処理の定義を正しく与える必要がある.本論文では新たにDSLとしてFMR(Feather-light MapReduce)を提案する.FMRで記述されたMap処理及びReduce処理は定理証明支援系Coqで検証可能であり,自動的にHadoop MapReduce上で実行可能なScalaのプログラムへと変換することが可能である.Hadoop MapReduceにおける典型的な処理に着目し,FMRでは効率的な逐次入出力を記述可能にした.著者のグループの先行研究で作成したMapReduceモデルを元に,FMRによる実装が仕様を満たすことを証明を用いて検証する.従来のCoq上におけるMapReduceモデルから得られる定義より,実行性能の低下を抑制する効果を評価した.また,FMRを用いることによる証明コストの上昇についても評価を行った.
- 2014-03-01
著者
関連論文
- マルチエージェントシステムにおけるメタデータを用いた協調プロトコル合成手法(モデル/理論,ソフトウェアエージェントとその応用論文)
- 適応エージェントのためのユビキタスコンピューティングミドルウェア(エージェント)
- CSTソリューションコンペティション2007及び2008の総括(ペトリネット,離散事象システム,一般)
- AI-2-1 CSTソリューションコンペティション2008 : 総括(AI-2.CSTソリューションコンペティション2008:表彰式・シンポジウム,ソサイエティ企画)
- AK-2-3 マルチカーエレベータ群管理アルゴリズムに関する研究動向 : CSTソリューションコンペティション2007の活動を通じて(AK-2.基礎・境界分野の研究最前線,ソサイエティ特別企画,ソサイエティ企画)
- CSTソリューションコンペティション2007 : 評価実験の詳細報告(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- AI-1-5 CSTソリューションコンペティション2007(総括)(AI-1. CSTソリューションコンペティション2007:表彰式・シンポジウム,依頼シンポジウム,ソサイエティ企画)
- モデリングは教育できるか?(要求/教育)
- 多数のノード取得攻撃に対応した無線センサネットワークにおける不正イベントの検知(センサネットワーク・P2Pネットワーク,ネットワークを支えるソフトウェア技術論文)
- プロセス間競合を考慮した自己適応システムの形式仕様構築
- Folksonomyマイニングに基づくWebページ推薦システム(エージェント応用システム,マルチエージェントの理論と応用)
- プロセス記述によるサービス合成のパーベイシブコンピューティングへの適用(モバイルコンピューティング)
- Webサービス連携のためのモバイルエージェント動作記述(オブジェクト指向とWeb技術)
- ソフトウェア論文座談会
- タグに関連づけられた時間・場所の概念抽出(「Webインテリジェンス」及び一般)
- 契約による設計を用いたインタラクションの実装(エージェント・アーキテクチャ,マルチエージェントの理論と応用)
- ゴール指向要求分析を用いたself-adaptiveシステムの構築
- 多数のノード取得攻撃に対応した無線センサネットワークにおける複製ノードの分散検知(センサネットワーク・P2Pネットワーク,ネットワークを支えるソフトウェア技術論文)
- 無線センサネットワークにおけるFalse Eventの検知(無線・モバイルネットワーク,情報洪水時代のネットワークサービス)
- variable-size DBFによる分散ハッシュテーブルのトラヒック量削減(モバイル/ユビキタス/P2P,ソフトウェアエージェントとその応用論文)
- Ringed Bloom Filterによる分散ハッシュテーブルのトラフィック量削減(ミドルウェア,マルチメディア,分散,協調とモバイル(DICOMO2006))
- 分散ハッシュテーブルにおけるAND検索時のトラフィック量削減(エージェント・アーキテクチャ,マルチエージェントの理論と応用)
- 無線センサネットワークにおける複数プログラムの動的配備
- モバイル環境向けエージェント移動制御方式の実装
- トップエスイー : サイエンスによる知的ものづくり教育
- Teaching how to write security target of Common Criteria using the i* methodology (ソフトウェア工学)
- 「コンピュータソフトウェア」における論文とは
- セキュリティソフトウェア工学の最前線
- IPEditor開発ツールとMobile UNITY言語の適用によるモバイルエージェントセキュリティの実現(オブジェクト指向技術)
- タグに関連づけられた時間・場所の概念抽出
- Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出(ソフトウェアシステム)