ISP Formal Verification Tool とは

ISP( "In-Situ Partial Order")は、ユタ大学のコンピューティングスクールで開発されたMPIプログラムの正式な検証のためのツールです。 SPINなどのモデルチェッカーと同様に、ISPはシステムの完全な状態空間で一連の安全性の特性を検証します。ただし、モデルチェッカーとは異なり、ISPはコードレベルの検証を実行します。つまり、ツールは、ビルド検証モデルなしで実際のプログラムコードを再生することによって、コンカレントプログラムのすべての関連インターリーブを検証します。このアイデアは、VeriSoftツールのGodefroidをはじめとするいくつかのツールで先駆けて開発されました。このジャンルの最近のツールには、Java Pathfinder、MicrosoftのCHESSツール、MODISTなどがあります。関連するインターリーブは、POEと呼ばれるカスタマイズされた動的な部分桁数削減アルゴリズムを使用して計算されます。
ISPは、デッドロックとアサーション違反のために最大14,000行のMPI / Cコードを正常に検証するために使用されています。現在、60を超えるMPI 2.1関数をサポートしており、MPICH2、OpenMPI、およびMicrosoft MPIライブラリでテストされています。
ISPは、LinuxおよびMac OS X用にダウンロードできます。 Windowsの下で実行するためのVisual Studioプラグインとして、そしてEclipseプラグインとして。