モデル検査器SPINにおける状態空間の性質の調査

  1. このページについて

    DSW07に投稿した論文 『モデル検査器SPINにおける状態空間の性質の調査』 で行った調査の詳細な結果を掲載している。

  2. 扱ったモデル

    BEEM: BEnchmarks for Explicit Model checkers にある promela モデルに対して、Spin を実行して検証を行う。
    今回は「invalid end state」の検証のみ。
    一部のモデルについては更にグラフの性質などを詳しく調査する。

  3. 実行結果

    実行結果(full) 実行結果(normal) 比較

  4. グラフの性質

    モデル一覧

    詳細(BFS) 詳細(DFS) : rev は探索の順番を逆にした結果

    取ったデータ(グラフ全般＆BFS)

    取ったデータ(DFS)

  5. モデル毎の比較