モデル検査ツール

1.概要

  Cプログラムの検査を行います。
  2つの検査ツール（MathSAT4を利用可能/使用しない)バージョンがあります。
  このツールの保証およびサポートは有りません。
  MathSATは本プロジェクトの成果物とは関係有りません。  
  MathSATを利用する場合はそれらのライセンス，使用条件に従ってください。
  
  MathSAT4はUniversity of Trentoで公開されている型式検査ソルバーで，
  学術環境における研究や評価の目的にのみ使用可能です。
  また、書面による許諾なしでは、特に商用製品の一部として使用するなど、
  商用環境で利用することはできません。 
  
  JST CREST「実用化を目指した組込みシステム用ディペンダブルオペレーティング
  システムの開発」(DEOS)プロジェクトのもと、東京大学によって開発されました。 


2.関連ファイル

  このファイル
    readme.txt
  モデル検査器（MathSAT4を利用しない通常版）
    sendagi.unstable.tgz
  モデル検査器（MathSAT4利用可能版）
    sendagi.with-mathsat.unstable.tgz


3.モデル検査器について
  mathsat利用可能版の方がより正確な検査ができる傾向にありますが
  実行時間は劣ります。
  動作確認はDebian Wheezyで行いました。
  多くのLinuxディストリビューションでも必要なパッケージを入れれば
  動作することと思います。
　　
3.1 必要なパッケージのインストール
  ここではインストールの概略を記します。詳細はtgzファイルのINSTALLを
  参照してください。
  
  
  # apt-get install -y ocaml-native-compilers libglpk-dev \
   ocaml-findlib libextlib-ocaml-dev libocamlgraph-ocaml-dev \
   libxml-light-ocaml-dev

3.2 ビルド方法（通常版）

  % tar xzf sendagi.unstable.tgz
  % cd sendagi
  % cp requirements/csisat-1.2.tar.gz .
  % tar xzf csisat-1.2.tar.gz
  % cd csisat-1.2
  % make
  % cd ../loligoedulis
  % make

3.3 実行方法（通常版）

  ./loligoedulis/clapがモデル検査器の本体プログラムです。
  実行オプションは
  
  % ./clap --help
  
  で見ることができます。

3.4 テストケース実行の例（通常版）

  実行には以下のパッケージが必要です。

  # apt-get install libounit-ocaml-dev

  テストツールを以下で作成します。

  % cd testsuite
  % make

  以下でテストを実行します。

  % cd ../test
  % CLAPDIR=(The directory where the model checker is located) sh ./run_test.sh
    (For example, CLAPDIR=../loligoedulis sh ./run_test.sh)

  テストは場合により数十分程度かかる場合があります。
  また現在のモデルチェッカーの制約により失敗する場合があります。