論文

査読有り
2014年3月

Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出(ソフトウェアシステム)

電子情報通信学会論文誌. D, 情報・システム
  • 姜 帆
  • ,
  • 田辺 良則
  • ,
  • 本位田 真一

97
3
開始ページ
625
終了ページ
634
記述言語
日本語
掲載種別
出版者・発行元
一般社団法人電子情報通信学会

Hadoop MapReduceはデータとしてキーと値による組を利用する大規模並列処理を行うためのフレームワークであり,今日では広く利用されている.目的の処理を行うため,Map及びReduce処理の定義を正しく与える必要がある.本論文では新たにDSLとしてFMR(Feather-light MapReduce)を提案する.FMRで記述されたMap処理及びReduce処理は定理証明支援系Coqで検証可能であり,自動的にHadoop MapReduce上で実行可能なScalaのプログラムへと変換することが可能である.Hadoop MapReduceにおける典型的な処理に着目し,FMRでは効率的な逐次入出力を記述可能にした.著者のグループの先行研究で作成したMapReduceモデルを元に,FMRによる実装が仕様を満たすことを証明を用いて検証する.従来のCoq上におけるMapReduceモデルから得られる定義より,実行性能の低下を抑制する効果を評価した.また,FMRを用いることによる証明コストの上昇についても評価を行った.

リンク情報
CiNii Articles
http://ci.nii.ac.jp/naid/110009804350
CiNii Books
http://ci.nii.ac.jp/ncid/AA12099634
ID情報
  • ISSN : 1880-4535
  • CiNii Articles ID : 110009804350
  • CiNii Books ID : AA12099634

エクスポート
BibTeX RIS