ホーム > 形式手法の概要 > 形式手法の例１（SPIN）

形式手法の例１（SPIN）

このページでは，形式手法・ツールの考え方，多様性を説明するための例として，SPINツールについてごく簡単に説明します．SPINは，形式手法において最も活用されているモデル検査と呼ばれる手法の代表的ツールです．SPINについての詳細は解説ページに別途まとめます．

SPIN概要

SPINは「モデル検査」と呼ばれる手法の代表的なツールです．モデル検査は，システムの振る舞い・状態変化に着目して，起きうる状態変化を網羅的に調べる手法です（性質を検証する方法による分類です）．検証する性質としては，「デッドロックが起きないか」「不具合のある状態に到達しないか」「期待していることが起きるか」といった実行の経過に関する性質を考えます．

簡単な例題

SPINの最も簡単な例題としては次のようなものがよく知られています．

  • プリンタ，スキャナがある．ユーザがそれらを利用する際には，それぞれにGetメッセージを送り利用権を確保する必要がある．プリンタ，スキャナともに，ある時点では高々１人のユーザにしか利用権を与えない（あるユーザに利用権を与えている間にはGetメッセージを受け付けない）．利用後にはPutメッセージにより利用権が解放される．

  • ユーザ１はプリンタ，スキャナの順にGetメッセージを送り両方を確保してタスクを実行する．終了後には同じ順にPutメッセージを送り解放する．

  • ユーザ２はスキャナ，プリンタの順にGetメッセージを送り両方を確保してタスクを実行する．終了後には同じ順にPutメッセージを送り解放する．

これはデッドロックの発生する典型的な例です．実行順序によっては，「ユーザ１はプリンタを確保してスキャナの確保を待ち，ユーザ２はスキャナを確保してプリンタの確保を待つ」という状況になりそれ以上進まなくなってしまいます．

SPINでは起きうる状態変化を網羅的に検査することにより，このデッドロックを検出することができます．その際にはまず，Promelaという言語を用いて並行に動作しているプロセスを定義します．例えば以下はユーザ１に相当するプロセスの定義の例です．

proctype P(){
  do :: channel2printer ! Get; channel2scanner ! Get ->
           skip; channel2printer ! Put; channel2scanner ! Put
  od
}

詳しいことはSPINの解説ページに記述しますが，ここではPという名前のプロセスの定義を行っています．このプロセスでは，まずプリンタ，スキャナへのチャネルからそれぞれGetメッセージを送信（記号 ! ）し，それらを確保しています．その後何か作業をして（今回の検査では重要ではないので skip としている），プリンタ，スキャナへのチャネルからそれぞれPutメッセージを送信し，それらを解放しています（チャネルやメッセージの定義は省略しています）．

このような感じで他のプロセスも定義してSPINツールに与えると，起きうる実行順序を網羅的に調べ，デッドロックに至る実行順序を検出することができます．

例題の補足

上の問題は非常に簡単な例でSPINのごく一部の機能しか用いていません．例えば複数プロセス間の実行順序による非決定性だけではなく，個々のプロセスに非決定的な動作を行わせることも可能です（エラーを起こしたり起こさなかったり，等）．また特に検証する性質については，LTL（Linear Temporal Logic，線形時相論理）という言語を用いてより多様な性質を記述することができます．LTLにおいては，例えば下記のような性質の記述を行うことができます．

  • 「リクエストを送ると，いつか必ず応答が返ってくる」
         [] (req => <> res)
    （どんな状態においても（ [] ），その状態でリクエストが発生している（req）ならば，以後いつか（ <> ）応答が発生している（res）状態に到達する）

  • 「初期化が終わるまでは常にリクエストを拒否する状態である」
         ! accepting U initialized
    （初期化が終わった状態（initialized）に，いつか到達しそれまでは（ U は until の意），リクエストを受け付ける状態（accepting）とはならない（ ! は否定））

（上記においてreq，res等はPromelaによるプロセス記述にラベルとして与えておく）

SPINは上記の問題のような資源制御（排他制御）のような問題や，通信プロトコルにおける同期制御等，並行システムの設計の検証によく用いられます．この場合，実装に入る前に設計の検証を行うことが多いですが，実装コードから一部の振る舞いを抜き出して検証するような場合もあります．

形式手法・ツールとしてのSPIN

大ざっぱにまとめると，形式手法・ツールとしてのSPINの特徴は下記のようになります．

システムのどの側面を形式化，記述？

並行プロセスが相互作用しながら実行していく振る舞い

システムのどのような性質を検証？

実行の経過に関する性質

性質をどのように検証？

起きうる状態変化の，ツールによる網羅的な検査

開発プロセスの中でどう位置づけ？

主に設計モデルの検証

バリエーション

ここで「モデル検査」という手法の分類は，性質を検証する方法に対する名称です．同じモデル検査であっても，ツールによって「検証できる性質」やその簡単さは変わってきます．また手法・ツールによっては「形式化，記述するシステムの側面」「検証する性質」として，実行によって経過する時間まで考えるものもあります．

このページの先頭へ戻る

形式手法の概要