形式手法（Formal Method）とSPIN
形式的手法による検証（ モデル検査法）関連の話題が周りで出ているが、いまいち自分は理解できていない。すこし時間をとってSPIN関連の書籍を読み合わさってみたので、忘れないようにまとめてみた。
■SPINで検証できる事。
- デッドロックが起きないか
- 期待した動作が行われるか
■検証するためにはどんな準備が必要？
- 論理的に正しい仕様を形式仕様記述で作成する（これに誤りがあれば検証段階で検出できる）。
ちょっと期待していたのとは違ったなあ（別な機会には使えそうだけど）。
やりたかったのは「他人が作成した仕様が論理的に正しいか」を検証したかったので、どちらかと使うべきツールはVDMみたい。ならつぎはVDMを学習しよう！
まとめ：
形式手法でもツールにより検証できる対象が違う。
そんなのはじめから気づけよと言われそうだけど、「形式手法によるモデル検査」という点で同じ種類と考えてしまった所がまずかったみたい。
