情報処理学会 第74回全国大会講演要旨

近年、大規模データ処理を効率的に行なうためのソフトウェアフレーム
ワークとしてMapReduceが注目されている。社会のIT化の進行と共に、
処理すべきデータの量は増大しており、今後MapReduceの重要性は益々
高まると考えられる。しかし、MapReduceによるデータ処理を安心・安全に
行なうには、それがきちんと整合性を保つことを検証できる手法が必要で
ある。特に我々は、開発者が上流の設計において、簡便かつ厳密な形で、
アプリケーションのアルゴリズムが正しいことを検証できる手法の確立が
重要であると考えた。そこで我々は、形式手法の一つであるモデル検査を
利用し、MapReduceに基づくアプリケーションのアルゴリズムを自動的かつ
網羅的に検証する手法を考案した。本稿ではその内容について報告する。