分散検証環境DiVinEを用いた分散LTLモデル検査アルゴリズムの性能比較

  1. このページについて

    分散検証環境 DiVinE を用いて分散 LTL モデル検査アルゴリズムの性能の比較を行う

  2. 比較するアルゴリズム

    DiVinE で実装されている以下のアルゴリズムについて比較を行う

    各アルゴリズムの詳細については http://anna.fi.muni.cz/divine/publications/index.html を参照のこと。

  3. 扱うモデル

    BEEM: BEnchmarks for Explicit Model checkers にある DVE モデルに対して、DiVinE を実行して検証を行う。
    検証する性質は LTL を使用したもののみ。
    各モデルの基本的な状態空間の性質はこちら

  4. 実験環境

    上田研クラスタ Folon-V (8 Node, 32 PEs)
    OS
    		 CentOS 4.4
    CPU
    		 Dual Core AMD Opteron 2.0 GHz × 2
    Memory
    		 4 GB
    Network 1000 BASE-T Ethernet
    MPI
    		 SCore 6.0.2

    今回は DiVinE 0.7.1 を使用

  5. 実験結果

    実験結果は結果のまとめページに

戻る