PPL2016 Poster

Posted on March 7, 2016

Actario: 定理証明支援系Coqによるアクターシステムの検証 (ポスター)

安武祥平，渡部卓雄
第18回プログラミングおよびプログラミング言語ワークショップ(PPL 2016), Mar. 7-9, 2016.

概要

アクターシステムの検証を目的とする，定理証明支援系CoqのライブラリActarioについて発表する．Actarioは以下のような特徴を持っている．

  1. アクターモデルを使った並行アプリケーションをCoqのDSLを用いて記述できる
  2. アクターモデルの意味論を提供しており，アクターモデル自体の性質を検証できる
  3. 作成したアプリケーションに対してその性質を検証できる
  4. 作成したアプリケーションをErlangのコードに変換できる

本発表では，主にActarioで記述されたアプリケーションの検証手法について説明する．