NuSMVによるモデル検査入門 (1) ステートマシンを定義する - Qiita

この前書いた記事はあまりにもやっつけだったので整理してみる。 概要 この記事は、シンボリックモデルチェッカNuSMV (http://nusmv.fbk.eu/) を使って、モデル検査を行うチュートリアルである。 NuSMVのバージョンはv2.6.0とする。バージョンによって機能がobsoleteされたり変更されたりするので、古いバージョン用の資料を読むときには注意されたい。 基礎知識 知ってるならスキップしてください。 モデル検査 (Model Checking) とは 状態遷移系が論理式を満たすかどうかを検査すること。 より正確には、あるKripke構造がある時相論理式を満たすか否かを検査することである。 一般に数理論理学で、データ構造 $M$ が論理式 $\phi$ を成り立たせる場合に $M\models\phi$ と書き「$M$ は $\phi$ のモデルである」と呼ぶことから、