Spin クイックリファレンス

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)

記号	意味	Spinでの記述
¬	pでない	!p
∧	pかつq	p && q
∨	pまたはq	p || q
→	pならばq	p -> q
↔	同値	<->
□	常にp	[]p
◇	いつか必ずp	<>
U	qまでpが成り立つ	p U q