「Spin クイックリファレンス」の版間の差分

2014年3月1日 (土) 19:30時点における最新版

Spinについて

Spinはモデル検査のためのツール。非同期、並列、分散アルゴリズムやシステムを対象とし検査する。 モデルの作成にはPromela言語を使用する。

コマンド

Spinのコードを実行する

spin a.pml

安全性の検証

spin -a -f '![]pp' ltl.pml
gcc -DSAFETY pan.c

オプション

-a

検証の用のソースコード(C言語)を生成する。

-e

すべてのエラーを表示する。

-cN

N番目のエラーで停止する。

-c0

エラーが発生したとき停止しない。

-m

通信チャンネルが一杯のとき、送信分はブロックせずに実効される。

メッセージは消失し通信チャンネルの状態は変わらない。

-t

ガイド付きのシュミレーションを実行する。

ログに関するオプション

-p

ソースコードを表示する

-g

グローバル変数を表示する

-s

チャンネルへのデータ送信を表示する

-r

チャンネルの受信データを表示する

モデルの作成

　検証対象のシステムモデルはPromela(Process Meta Language)で記述する。

• Promelaの文法

時相論理(LTL)