Scalaの並行プログラム検査における状態空間探索手法

• Item type: Symposium(1)
• 公開日: 2014-08-25
• タイトル: Scalaの並行プログラム検査における状態空間探索手法
• タイトル / 言語: en
• タイトル: A state space exploration technique for verifying concurrent programs in Scala
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 形式手法
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 東京大学
• 著者所属: 東京大学
• 著者所属: 国立情報学研究所
• 著者所属: 国立情報学研究所
• 著者所属: 東京大学／国立情報学研究所
• 著者所属(英): en
• 著者所属(英): The University of Tokyo
• 著者所属(英): en
• 著者所属(英): The University of Tokyo
• 著者所属(英): en
• 著者所属(英): National Institute of Informatics
• 著者所属(英): en
• 著者所属(英): National Institute of Informatics
• 著者所属(英): en
• 著者所属(英): The University of Tokyo / National Institute of Informatics
• 著者名: 島田, 工; 前澤, 悠太; 鄭, 顕志; 田辺, 良則; 本位田, 真一
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: アクターモデルは，広く利用されている並行プログラミングモデルの 1 つであり，各 Actor の独立性に着目することで効率的に検証を行う手法が提案されてきている．しかし，Scala 言語による現実世界のプログラムでは，しばしば純粋なアクターモデルは用いられず，他の並行モデルが併用される．この場合には既存手法は適用できない．本研究ではアクターモデルと併用されることの多い Future 等が存在する場合でも，検証を可能にする手法を提案する．実験結果は，既存手法では検出が難しかった不具合が提案手法で発見できることを示しており，より多くの並行プログラムに対して不具合発見を支援できるようになったと考えられる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Actor model, one of widely used concurrent programming models, has efficient verification methods focusing on the independence of each actor. However, Scala programs in the real world often use actor model together with other concurrency models instead of the pure actor model. Such applications cannot leverage existent methods. In this research, we propose a verification method that can apply to programs which use actor model and Future, which is often used together with actor model. From our experiment results, our method could detect bugs in the subject programs which are difficult for the existent methods to verify and we consider this method can help bug detection in wider range of concurrent programs.
• 書誌情報: ソフトウェアエンジニアリングシンポジウム2014論文集; 巻 2014, p. 54-59, 発行日 2014-08-25
• 出版者 / 言語: ja
• 出版者: 情報処理学会