モデル検査ツール一覧

この記事では、モデル検査ツールを一覧表示し、それぞれの機能の概要を説明します。

以下の表には、

1. ダウンロード可能なウェブサイト、
2. 宣言されたライセンス、
3. アーカイブされた文献に掲載された記述、
4. それについて説明したウィキペディアの記事。

以下の表では、次の略語が使用されています。

• 同等性：
  • SB: 強双模倣性
  • WB: 弱い双模倣
  • BB: 分岐双模倣
  • STE: 強力微量等価性
  • WTE: 弱トレース等価性
  • 私：5月の同等性
  • 私：同等性必須
  • OE: 観察的等価性
  • SE: 安全性の同等性
  • t*E: τ*.a 等価性
• ソフトウェアライセンス:
  • FUSC：特定の条件付きで無料（例：研究者は無料）

• CCSP: CSPのいくつかの演算子を組み込むことによってCCSから得られるプロセス計算。Olderog ^{[ 1 ]}とvan Glabbeek/Vaandrager ^{[ 2 ]}によって定義されている。
• CSP：Communicating sequential processes（通信シーケンシャルプロセス）。並行システムにおける相互作用パターンを記述するための形式言語。FDR2はCSPの改良チェックツールであり、2つのモデルの互換性を比較する。
• DVE入力言語：システムは、共有変数とバッファなしチャネルを介して通信する拡張有限状態機械のネットワークとして記述されます。バッファ付きチャネルや、受信処理を実行せずに受信するメッセージの種類をチェックする機能はサポートしていません。
• FC2：（Common Format V2）同期型（階層型）オートマトンネットワークのマシンレベルASCII表現。1992年のEsprit基礎研究活動CONCURで定義。主にプロセス代数の分野において、多くの検証ツールの入力および交換フォーマットとして使用されている。
• FSP：インペリアル・カレッジで定義された有限状態プロセス言語。
• Java：オブジェクト指向プログラミング言語。
• LNT: LOTOS New Technology。プロセス計算、関数型プログラミング言語、命令型プログラミング言語に触発された仕様記述言語。LNTは、LOTOSおよびE-LOTOSの現代的な代替として設計されました。
• LOTOS：時間順序仕様言語（ISO規格8807）。ISO OSI規格におけるプロトコル仕様に使用される、時間順序に基づいた形式仕様言語。
• mCRL2：並行離散イベントシステムを記述するための仕様記述言語。
• Murφ：ガード付きコマンドと非同期インターリーブ型の並行処理モデルを採用し、すべての同期と通信はグローバル変数を介して行われます。
• PEPA：パフォーマンス評価プロセス代数。コンピュータシステムや通信システムをモデル化するために設計された確率過程代数です。
• Plain MC: MRMCおよびPRISMで使用されるシンプルなテキストファイル形式。
• Promela：プロセスまたはプロトコルメタ言語。検証モデリング言語です。この言語を使用すると、例えば分散システムをモデル化するために、並行プロセスを動的に作成できます。
• Starlark：Starlarkは、GoogleがBazel向けに開発したPythonの方言です。FizzBeeなどのモデルチェッカーは、モデリング言語としてStarlark/Pythonを使用します。
• TLA+：時間論理に基づく汎用仕様記述言語で、元々は分散システムや並行システム向けに開発された。仕様とそのプロパティを記述する言語は同じである。

• AFMC: 交替なしモーダルμ計算。
• アサーション：命令型のアサーション文。
• CSL（連続確率論理）は、連続時間マルコフ過程の双模倣性を特徴づける。
• CSRL：連続確率報酬論理。報酬構造（いわゆるマルコフ報酬モデル）で拡張された連続確率マルコフ連鎖（CTMC）上の尺度を指定するための論理。
• CTL：計算ツリー論理。分岐時間論理の一種であり、その時間モデルはツリー状の構造で、未来は確定しておらず、未来には様々な経路が存在し、そのいずれもが実際に実現する経路となり得る。
• 不変条件：システム状態に関する述語。
• LTL：線形時相論理。時間に関する様相を持つ様相時相論理。
• MCL: モデル検査言語。ユーザーフレンドリーな正規表現と値渡し構造で拡張された、選択のない様相μ計算。CTLとLTLを包含する。
• mCRL2 mu-calculus: Kozen の命題様相 μ-calculus (原子命題を除く) に、データ依存プロセス、データ型に対する量化、多重アクション、時間、および正規式を追加した拡張版。
• PCTL：確率的CTL。記述された特性を確率的に定量化することを可能にするCTLの拡張版。
• PLTL：確率的線形時相論理。
• PRCTL：確率的報酬計算ツリーロジック。PCTLに報酬制限特性を追加した拡張版。
• PSL：プロパティ仕様言語
• SVA: SystemVerilog標準アサーション言語のサブセットであり、IEEE 1800として標準化されている。
• XTL：拡張時間言語。アクションベース、明示的状態、値渡し型のモデルチェッカーを迅速に実装するためのドメイン固有言語。

• アルタリカ

• 検証および合成ツールの一覧（GitHub上の公開リポジトリ）
• 確率的、確率的、ハイブリッド、および時間付きシステムのための検証ツールのリスト

共通のベンチマーク

• MCC（モデル検査コンテストのモデル）：多くの学術的および産業的事例研究から生まれた、数百ものペトリネットのコレクション。
• VLTS（Very Large Transition Systems）：サイズが徐々に大きくなるラベル付き遷移システムのコレクションで、多くの科学論文で使用されています。