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

IPSJ

Bibliographic Information

Other Title
  • A state space exploration technique for verifying concurrent programs in Scala

Abstract

アクターモデルは，広く利用されている並行プログラミングモデルの 1 つであり，各 Actor の独立性に着目することで効率的に検証を行う手法が提案されてきている．しかし，Scala 言語による現実世界のプログラムでは，しばしば純粋なアクターモデルは用いられず，他の並行モデルが併用される．この場合には既存手法は適用できない．本研究ではアクターモデルと併用されることの多い Future 等が存在する場合でも，検証を可能にする手法を提案する．実験結果は，既存手法では検出が難しかった不具合が提案手法で発見できることを示しており，より多くの並行プログラムに対して不具合発見を支援できるようになったと考えられる．

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.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

  • CRID
    1050292572154197760
  • NII Article ID
    170000084817
  • Web Site
    http://id.nii.ac.jp/1001/00102830/
  • Text Lang
    ja
  • Article Type
    conference paper
  • Data Source
    • IRDB
    • CiNii Articles
    • KAKEN

Report a problem

Back to top