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