ヌーSMV
| ヌーSMV | |
|---|---|
| 開発者 | FBK-irst（トレント、イタリア）、CMU（ピッツバーグ、ペンシルベニア州）、ジェノバ大学（イタリア）、トレント大学（イタリア） |
| 安定版リリース | |
| 書かれた | ANSI C |
| オペレーティング·システム | Linux、Mac OS X、Microsoft Windows |
| タイプ | モデル検査 |
| ライセンス | LGPL v2.1 |
| Webサイト | nusmv.fbk.eu |
コンピュータサイエンスにおいて、NuSMVは、二分決定図（BDD）に基づく最初のモデル検査ツールであるSMVシンボリックモデルチェッカーの再実装および拡張です。 [ 2 ]このツールは、モデル検査のためのオープンアーキテクチャ として設計されています。これは、産業規模の設計の信頼性の高い検証、他の検証ツールのバックエンドとしての使用、および形式検証技術の研究ツールとしての使用を目的としています。
NuSMV は、ITC-IRST ( Istituto trentino di cultura in Trento )、カーネギーメロン大学、ジェノヴァ大学、トレント大学の共同プロジェクトとして開発されました。
NuSMVのバージョン2であるNuSMV 2は、NuSMVのすべての機能を継承しています。さらに、BDDベースのモデル検査とSATベースのモデル検査を組み合わせています。[ 3 ]これは、ITC-IRSTの後継組織である Fondazione Bruno Kesslerによって保守されています。
機能
NuSMVは、計算木論理（CTL）と線形時相論理（LTL）で表現された仕様の解析をサポートします。バッチモード、またはテキスト形式のユーザーインターフェースを用いた対話型モード で実行できます。
NuSMV を対話的に実行する
NuSMV のインタラクション シェルは、次のようにシステム プロンプトから起動されます。
[システムプロンプト]$ NuSMV -int NuSMV> go NuSMV>NuSMVはまず、初期化ファイルが存在し、-sかつコマンドラインで渡されない限り読み取り可能な場合、そのファイルからコマンドを読み取って実行しようとします。ファイルmaster.nusmvrcは、環境変数で定義されたディレクトリ内NUSMV_LIBRARY_PATH、またはそのような変数が定義されていない場合はデフォルトのライブラリパス内で検索されます。そのようなファイルが存在しない場合は、ユーザーのホームディレクトリと現在のディレクトリもチェックされます。初期化ファイル内のコマンドは順番に実行されます。初期化フェーズが完了すると、NuSMVシェルプロンプトが表示され、システムはユーザーコマンドを実行できる状態になります。
NuSMVコマンドは通常、コマンド名と呼び出されるコマンドの引数で構成されます。コマンドラインオプションを使用することで、NuSMVにファイルから一連のコマンドを読み込ませて実行させることも可能です-source。
[システムプロンプト]$ NuSMV -source cmd_file NuSMVバッチの実行
-int オプションを指定しない場合、NuSMV は次の形式のバッチ プログラムとして実行されます。
[system_prompt]$ NuSMV [コマンドラインオプション] input_file LTL仕様またはCTL仕様の確認
NuSMVは、与えられたLTL制約またはCTL制約が与えられたモデルに当てはまるかどうかを確認するために使用できます。例えば、次のようなCTL仕様を確認したいとします。
CTLSPEC EF ( proc5 . state =クリティカル);stateこの仕様は、プロセスのコンポーネントがいずれかの時点でproc5値を持つような実行パスが存在する場合に真となりますcritical。ユーザーは、以下のコマンドを使用して、モデルがこの仕様に当てはまるかどうかを確認できます。
[system_prompt]$ NuSMV [コマンドラインオプション] input_file NuSMV> go NuSMV> check_ctlspec仕様が正しい場合、NuSMVはあなたに通知します
-- 仕様 EF proc5.state = critical が true > NuSMV何らかの仕様が失敗した場合、NuSMV は、可能であれば、失敗の原因を示す実行の完全なトレースを返します。
参照
- Spin Model Checker は非同期ソフトウェアシステム用の汎用モデルチェッカーです。
- CADP（分散プロセスの構築と分析）、非同期並行システムの形式設計のためのツールボックス
参考文献
- ^ 「バージョン 2.7.0」。NuSMV （プレスリリース）。Fondazione Bruno Kessler。2024年10月25日。
- ^ KL McMillan. シンボリックモデル検査. Kluwer Academic Publ., 1993.
- ^ A. Biere, A. Cimatti, E. Clarke , Y. Zhu. BDDを使用しない記号モデル検査. システム構築と分析のためのツールとアルゴリズム, TACAS'99, 1999年3月.
外部リンク
- NuSMVウェブサイト
- Nuseen Web サイト: モデル チェッカー NuSMV 用の Eclipse ベースのツール セット。
- nuXmv : SMTベースの検証と更新されたSAT解決技術でNuSMVを拡張します
