Loading article…
Murφ（/ˈmɝ.fi/、Murphi とも綴られる）は、スタンフォード大学で開発された明示的状態モデルチェッカーであり、キャッシュコヒーレンスプロトコルの形式検証に広く使用されている。
Murφ の初期の歴史は、David Dill の論文で説明されています。[ 1 ] Murφ の最初のバージョンは、1990 年と 1991 年にスタンフォード大学で David Dill 教授と彼の大学院生の Andreas Drexler、Alan Hu、Han Yang によって設計され、主に Andreas Drexler によって実装されました。仕様言語は、David Dill、Alan Hu、C. Norris Ip、Ralph Melton、Seungjoon Park、Han Yang によって大幅に修正および拡張されました。Ralph Melton は、1992 年の夏と秋に新しいバージョンを実装しました。Seungjoon Park は、生存チェックと公平性制約を追加しましたが、生存検証のアルゴリズムが重要な最適化、特に対称性削減と競合したため、生存検証は後続のリリースでは省略されました。C. Norris Ip は、可逆ルールと繰り返しコンストラクタ (リリース 3.1 には含まれていません) を実装し、対称性と多重集合削減 (含まれています) を追加しました。 Ulrich Sternはハッシュ圧縮を実装し、[ 2 ]ディスクの使用を改善し、並列Murφを実装した。
スタンフォード大学からの最後のリリースは、1993年11月にリリースされたバージョン3.1でした。それ以降、他のグループによってMurφの派生バージョンが数多く作成されています。
Murφコンパイラは、Murφ仕様言語で記述されたモデルを受け取り、そのモデルの検証器となるC++コードを出力します。（つまり、C++コードを実行すると、仕様で記述された設計に対して明示的な状態モデルチェックが実行されます。） Murφ仕様言語は、ガード付きコマンドと非同期インターリーブ並行処理モデルを使用し、すべての同期と通信はグローバル変数を介して行われます。検証器は、モデルで指定されている不変条件と内部アサーションの形で安全性プロパティをチェックし、デッドロックをチェックします。活性プロパティはチェックしませんが、Murφリリース2.7Lでは、一連の一般的なLTL活性プロパティの検証がサポートされていました。言語と検証器は、いくつかの種類の対称性削減をサポートしています。[ 3 ]
Murφは元々キャッシュコヒーレンスプロトコルの検証に適用されていましたが[ 4 ] 、セキュリティプロトコルの検証など他の問題にも適用されています。
MurφのライセンスはMITライセンスに類似しています。Murφは、著作権表示とライセンスを含めること、スタンフォード大学の名前を許可なく広告や宣伝に使用しないこと、および許可なく改変版をMurphiと呼ばないことを条件に、あらゆる目的で使用、複製、改変、販売、再配布することができます。
Murφの派生バージョンは、スタンフォード大学をはじめとする様々な場所で数多く作成されており、以下のようなものがある。