モデル検査とSPIN入門

SEA関西支部プロセス分科会(略称SEA関西SPIN)に参加しました。
トゥルーロジックの野中さんはUNIXカーネルの開発者たちが開発したSPINの解説でした。SPINは状態遷移を検証する処理系で、モデルが取りうる状態と起きてはいけない状態の論理積が空であることをすべての状態を展開して確認します。モデル検証は実装の前に設計を検証するもので、自動、反例を示す、まれにしか起きない問題を検証するといった特徴があります。

言語はPROMELAといい、do-od、if-fiとさすがにUNIXの開発者が作っただけあってshのような表記です。いつかきっとは" <>"、いつもずっとは"[]"、untilは"Ｕ"です、このうち、" <>"をひし形はいつかきっと傾くという説明がGOODでした。

モデル検証はアルゴリズムと計算機の高速化で1980年に7日かかったものが今では数秒で処理できるようです。SPINにはモデル検査のCコードを出力する機能もあるそうです。
詳細とツールは、http://www.spinroot.com/にあるようです(私は見れませんでした)。

SRA-KTLの岸田さんは「銀河ヒッチハイクガイド」をつかみに、岸田さんが70年代後半にアメリカのSRAでエドワードミラーと知り合って、カバレージを日本に伝えたお話、LehmanのS(Specificationが定義できる),P(なんとかプログラマブル),E(Embedded)のお話、社会のチリにまみっれているからと大森荘蔵に教えを受けられなかったお話、ソシュールが言語学は規範の額ではない(正しい日本語とか)と同じく、ソフトウェア工学は規範の額ではなく、モデル(文字)はソフトウェア(言語)の正体を隠すものであって、モデルを剥ぎ取ったところに本物のソフトウェアが現れる、E-typeは無限の属性を持つので、仮説は2000年問題のように成り立たなくなる、といったお話で構成されていました。

最後のディスカッションでは、SPINは特定領域に絞って使う、複数の形式手法を組み合わせないといけないのが現状といったわだいが出ていました。