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

安武, 祥平  ,  Yasutake, Shohei  ,  渡部, 卓雄  ,  Watanabe, Takuo

2016-03
Description
アクターシステムの検証を目的とする,定理証明支援系CoqのライブラリActarioについて発表する.Actarioは以下のような特徴を持っている.(1)アクターモデルを使った並行アプリケーションをCoqのDSLを用いて記述できる.(2) アクターモデルの意味論を提供しており,アクターモデル自体の性質を検証できる.(3) 作成したアプリケーションに対してその性質を検証できる.(4) 作成したアプリケーションをErlangのコードに変換できる.本発表では,主にActarioで記述されたアプリケーションの検証手法について説明する.

Number of accesses :  

Other information