応用情報システム工学演習 (2026)

内容

nuXmvで学ぶモデル検査

プログラムや制御器について，「危険な状態に入らないだろうか」「要求に対して応答できるだろうか」と考えることがあります．この教材では，システムの振る舞いを状態と遷移で表し，nuXmvを使って性質を検証します．

小さな例を実行するところから始め，モデルの記述，性質の記述，反例を使った修正，状態空間の簡略化，有界モデル検査（BMC）へと進みます．

第1回を始める

学習のゴール

このチュートリアルを終えたとき，次のことができるようになることを目指します．

自然言語の説明から，小さな状態遷移モデルを作る．
安全性と活性を区別し，検証する性質を記述する．
バッチ実行とインタラクティブ実行を使い分ける．
反例から問題を特定し，モデルを修正する．
状態空間が大きくなる理由を説明し，モデルを簡略化する．
BMCの探索上限を指定し，結果の意味と限界を説明する．

全6回の学習計画

全6回の資料を掲載しています．発展演習や総合演習は，必要に応じて授業後の自己学習にも使ってください．

回	内容	主な演習	公開状況
第1回	モデル検査の考え方，導入，最初のバッチ実行	正常なモデルとバグのあるモデルを比較し，反例を読む	作成済み
第2回	状態遷移図からSMVモデルを書く	初期状態・次状態・条件分岐・非決定性を記述する	作成済み
第3回	安全性・活性・反例による修正	性質を記述してバグを修正し，空虚な成立を考える	準備中
第4回	対話的な実行，環境入力，モジュール	環境と制御器を組み合わせて調べる	準備中
第5回	状態爆発とモデルの簡略化	値域や変数を見直し，変更前後を比較する	準備中
第6回	BMCと総合演習	探索上限を変えて反例を探し，結果の意味を説明する	準備中

必要な前提知識

変数，条件分岐，真偽値（Boolean）についての基本的なプログラミング知識を使います．論理式の「かつ」「または」「否定」が分かれば始められます．時相論理やモデル検査の経験は必要ありません．

実行環境

Windowsを基本とし，macOSでも同じSMVモデルを使用します．コマンドが異なる箇所は，Windows（PowerShell）／macOS（Terminal）のタブから選んでください．タブを選ぶと，ほかの箇所でも同じOSの手順が選ばれます．

教材の基準バージョンは nuXmv 2.1.0 です．公式の旧バージョン配布ページにはWindows x86_64版とmacOS universal版が掲載されています．2026年10月8日の公式ダウンロードページでは2.2.0のWindows版は準備中のため，両OSでバージョンをそろえます．

資料の使い方

各回の「到達目標」を読む．
説明と図を確認し，指示されたコードやコマンドを実行する．
出力を期待結果と比較し，違う場合はトラブルシューティングを確認する．
演習では，実行前の予想と実行後の観察を分けて考える（メモや紙に書き出すとよい）．
ヒントと解答例は，まず自分で考えてから開く．
各回の最後の「振り返り」を使い，理解が曖昧な箇所を復習する．

成果物の提出は求めません．演習の解答例と解説を使い，結果の理由を自分で説明できるかを確かめながら進めます．演習メモは任意です．

コードブロックのコピーボタンを利用できます．出力例やプロンプトは，実行するコマンドに含めないでください．

共通の題材：要求と応答の制御器

待機している制御器に要求が来ると，処理を行い，応答して待機に戻ります．授業を進めながら環境入力や構成要素を追加します．第1回では振る舞いを読むことに集中できるよう，要求が毎回到着する簡単な周期モデルを使います．

flowchart LR
    A[待機] -->|要求| B[処理]
    B -->|処理完了| C[応答]
    C --> A

検証結果を読むときの注意

trueは，検証した性質が作成したモデルとその仮定のもとで成立したことを表します．実システムについて結論を出すには，モデルが必要な振る舞いを表しているか，性質が要求を適切に表しているかも確認します．

falseは性質を満たさない振る舞いがあることを表します．反例を読むと，どのように違反に至ったかを調べられます．構文エラーや実行失敗とは区別してください．

公式資料

教材では入門に必要な部分から説明します．コマンドの詳細を確認する場合は，使用しているバージョンの配布物に含まれるマニュアルも参照してください．