« モデルを検査! | トップページ | モデル検査 調べ中。 »

SPINを使うモデル検査に思うこと。

SPINでは、

状態遷移モデルをPromelaで、

検査項目をLTLで、

それぞれ記述する。

Promelaは、シェルスクリプトに似た言語だ。

C言語にも似ている。

こんな風に書く(↓)。

active proctype hello()
{
  do
    if
    ...
    fi
  od
}

LTLは、"Linear Temporal Logic"の略で、

線形時相論理の論理式だ。

こんな風に書く(↓)。
[](p -> <>q)

で、Promelaで書いた状態遷移モデルの全パスを調べて、

LTLで書いた論理式が成立するかしないかを調べる。

成立しない場合は、反例を一つ提示する。

全パスを調べるので、

部分的な検証に過ぎないテストより確実に、

モデルの検証ができる。

要求分析をPromelaとLTLでするとして、

どうやって実装言語とつなげていくのかが、

やっぱり気になる。

★WOZ★

|

« モデルを検査! | トップページ | モデル検査 調べ中。 »

ソフトウェア」カテゴリの記事

コメント

コメントを書く



(ウェブ上には掲載しません)


コメントは記事投稿者が公開するまで表示されません。



トラックバック

この記事のトラックバックURL:
http://app.f.cocolog-nifty.com/t/trackback/1286769/32106177

この記事へのトラックバック一覧です: SPINを使うモデル検査に思うこと。:

« モデルを検査! | トップページ | モデル検査 調べ中。 »