|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。
SPINモデルチェッカ（英: SPIN model checker）は、ソフトウェアのモデル検査のためのツールである。Gerard J. Holzmann らが開発し、15年以上に渡って改良を続けてきた。2001年にAssociation for Computing Machinery (ACM) のソフトウェアシステム賞を受賞している。1995年以来、ほぼ毎年モデル検査に興味のある SPIN ユーザーや研究者による SPIN ワークショップが開催されている。 == 概要 == SPIN(Simple Promela INterpreter)は、オートマトンに基づく模型検査器(model checker)。検査対象のシステムは専用の言語Promela (Process Meta Language) で記述される。Promela は、非同期分散アルゴリズムを非決定的オートマトンとしてモデル化する。検証される属性は線形時相論理の論理式で表される。この論理式の否定形をBüchiオートマトンに変換して Promela のモデルと合成し、モデル検査アルゴリズムの一部とする。モデル検査の他に、SPIN はシミュレータとしても操作可能であり、システムのとりうる実行経路の1つを実行し、そのトレース結果をユーザーに示す。 多くのモデルチェッカとは異なり、SPIN はモデル検査そのものを実施するわけではなく、その問題に固有のモデルチェッカのC言語ソースを生成する。このような若干古い技法を使うことでメモリ使用量を削減し、性能を向上させると共に、モデルにユーザーが自由にCのコードを追加できるという利点がある。SPIN では性能向上やメモリ使用量削減のために以下のような様々なオプションを用意している。 * 半順序法（partial order reduction） * 状態データ圧縮 * ビット状態ハッシング（状態情報全体を格納するのではなく、ハッシュコードをビットフィールドで記憶する。完全性は犠牲になるが、メモリを大幅に削減できる） * 弱い公平性の施行（weak fairness enforcement） GUI として XSpin，JSpin，iSpin が準備されている。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「SPINモデルチェッカ」の詳細全文を読む スポンサード リンク
|