SMV入門(全10回)

開発深知」からSMV入門の講義動画を紹介します。動画をご覧になるには、開発深知の会員登録(無料)が必要です。

講義概要

モデル検査ツールSMV、状態遷移図について学習する講義です。講義は、動画と小テストの構成になっております。

講義は、こちらから登録することができます。
SVM入門 | 開発深知

本講義の目標

本講義は、モデル検査器SMVを用いて独力でモデル検査を実行できる技術について習得することを目的としています。具体的には、専用言語であるSMV言語の文法の習得、検査式の作成方法の習得、モデル検査器SMVの操作方法の習得を目指します。

講義では「SMV(Symbolic Model Verifier)とは何か?」という基本的な部分から解説し、小テストを通して理解を深めていく構成となっています。
01_本講義について

本講義の構成

SMVとは
SMVの概要、SMVの種類、SMV専用言語の文法の種類、検査式について解説します。
状態遷移図_1
状態線地図の概要、状態の数とパスの数、変数ごとの状態遷移図について例題などを通じて解説します。
状態遷移図_2
変数ごとの状態遷移図の作成方法、状態の列挙、初期状態の指定、遷移状態の指定、遷移条件の記述について解説します。
SMV言語_1
SMVファイルの構成、変数宣言、宣言した変数の初期状態(初期値)の設定、宣言した変数の状態遷移系の記述、演算子(種類・優先順位、ならばなど)、よくあるミスについて解説します。
SMV言語_2
状態遷移図からのモデルのコーディング、変数宣言、初期値の設定、状態遷移系の記述、例題(キュー)について解説します。
SMV言語_3
SMV言語についての応用、initとnextの概要、initとnextを用いる場合と用いない場合の違い、DEFINE、CadenceSMVの独自文法について解説します。
CTL式_1
CTL式の基本パターン、基本パターンごとのTRUEとなる場合、およびFALSEとなる場合について解説します。
CTL式_2
CTL式の真偽の相互関係、CTL式の変換、CTL式と否定(!)の関係、Spec Patternsについて解説します。
CTL式とLTL式
CTL式とLTL式の構成、パス限量子、様相演算子、検査式の記述方法、よく使う検査式について解説します。
SMVの操作
CadenceSMV、NuSMV、到達可能状態数の算出方法について解説します。

本講義の構成

講師

株式会社フォーマルテック
早水公二先生
※講座内容や講師の所属に関しましては、収録時の情報を掲載しております。変更になっている場合がございますので、ご了承いただきますようお願いします。

講義スライド

SMV入門の講義からスライドをピックアップしてご紹介します。

SMVとは

02_SMVとは

SMVとは?
モデル検査(ツール)の1つ
SMV→Symbolic Model Verifier(記号モデル検査)
状態遷移系を論理式に変換して、論理積や論理和などの記号処理を用いてモデル検査を実行
(状態を1つずつ総当たりで検査するのではない)
内部のデータ構造はBDD→Binary Decision Diagram(二分決定グラフ)
巨大な状態遷移系でも完結にグラフの形で表現できる

  • 記号処理により検査の実行速度が高速
  • BDDを採用することで大規模なシステムでも検査が可能

SMVの種類

03_SMVの種類

商業利用:企業などの営利団体での利用
 例)製品にモデル検査を適用
商用可能なSMVは「NuSMV」だけである
全て無償で配布されている→確実な動作保証は無い(不具合も存在する)

本講義では

04_本講義では

  • モデル検査器→CadenceSMVを用いて説明(GUIが有るため)
  • 文法→共通文法について技術習得
  • 検査式→主としてCTL式の技術習得(CTL式が解ればLTL式は容易)

企業や組織等で商用利用する場合は必ず「NuSMV」を利用すること
NuSMVは商用利用可能で共通文法が使用できる。

SMVを用いたモデル検査では状態遷移系が基本

05_SMVを用いたモデル検査では状態遷移系が基本
重要

  • 検査対象の振る舞いを必ず状態遷移図で表現する
     →状態遷移図はモデルの設計図である
     →コーディングの前に設計図を作成する
     →慣れれば省略可能であるが十分に注意する
  • 状態遷移図には作成ルールがある
  • SMV言語の文法は他のプログラミング言語と比較して簡単
     →状態遷移図が正確であれば適切なモデルを作成できる

状態遷移図=有限個の状態+有限個の遷移関係

06_状態遷移図=有限個の状態+有限個の遷移関係
※行き止まりは禁止!(状態Cのループは自状態への遷移で行き止まりではない)
※遷移関係には遷移条件を記述しない

パスの例

  • 状態A→状態B→状態C→状態D→状態A・・・
  • 状態A→状態B→状態C→状態B→状態C・・・
  • 状態A→状態B→状態C→状態C→状態C・・・

変数毎の状態遷移図の作成方法

146408_変数毎の状態遷移図の作成方法_SMV入門
例)変数Stateが4つの状態st1、st2、st3、st4を持つ場合

変数Stateの振る舞い(仕様)

  1. 初期状態はst1である
  2. st1の状態で遷移条件1が成立するとst2に遷移する
  3. st1の状態で遷移条件2が成立するとst3に遷移する
  4. st1の状態で遷移条件3が成立するとst2に遷移する
  5. st2の状態からは任意にst3あるいはst4に遷移することがある
  6. st3の状態になれば必ず初期状態に戻る
  7. st4の状態で遷移条件1が成立するとst2あるいはst3に遷移する
  8. st4の状態で遷移条件が不成立なら必ず初期状態に戻る

仕様を熟読して行間を補足する→次頁

変数の状態遷移を記述する

146409_変数の状態遷移を記述する_SMV入門
常に状態遷移図を見ながら記述する。

SMVファイルの構成(initとnextについて)

146410_SMVファイルの構成(initとnextについて)_SMV入門

CTL式の基本パターン

146411_CTL式の基本パターン_SMV入門

基本パターン 意味
AG(P) 全てのパスにおいて、全ての状態でPが成立する
AX(P) 全てのパスにおいて、次の状態でPが成立する
AF(P) 全てのパスにおいて、将来のある状態でPが成立する
A[P U Q] 全てのパスにおいて、Qが成立する状態よりも前の状態までPが成立する状態が続く
EG(P) あるパスにおいて、全ての状態でPが成立する
EX(P) あるパスにおいて、次の状態でPが成立する
EF(P) あるパスにおいて、将来の状態でPが成立する
E[P U Q] あるパスにおいて、Qが成立する状態より前の状態までPが成立する状態が続く

CTL式の諸規則_1

146412_CTL式の諸規則_1 CTL式の真偽の相互関係_SMV入門

CTL式とLTL式の構成

146413_CTL式とLTL式の構成_SMV入門

検査実行(Verify all)

146414_検査実行(Verify all)_SMV入門

関連講義

SMV入門の関連講義について紹介します。

SMVで学ぶモデル検査入門
本セミナーでは、モデル検査の概要に加えて、企業での取り組みやデモ、多くの例題を交えながら初心者の方にも分かりやすく説明します。また、演習問題も用意していますので、実際にモデル検査ツールSMVを操作することで、より深い理解を得ることができます。具体的には、モデル検査とは何かやSMVへの出力(変数毎の状態遷移図)等について解説していきます。
設計モデル検証(応用)
本講座では、代表的な3つのモデル検査ツールであるSPIN、SMV、およびLTSAに対し、まず標準のモデル記述言語UMLを全面的に採用し、実際に3つのツールの利用を通して、ソフトウェア設計検証の難しさを体感した上で、設計モデルの特徴に合わせたモデル検査ツールの使い分け、およびノウハウを習得していきます。また、本講義を受講する前に、設計モデル検証(基礎)の講義を受講しておくと理解が深まります。
基礎理論
形式手法を知る上で必要となる基礎知識について学んでいく講義です。形式手法入門としてもご覧いただけます。第15回:ツール概説にて、モデル検査ツール(SPIN、SMV、LTSA、UPPAAL)について解説しています。
モデル検査事例演習
本講座は、モデル検査の実務を想定し、その開始から終了までの全プロセスを意識した演習を行います。第3回:モデルのコーディングでは、例題を元に変数、状態遷移図の作成についてモデル検査器のSMVを元に解説しています。

参考リンク

トップエスイー | サイエンスによる知的ものづくり教育プログラム
NPO法人トップエスイー教育センター
トップエスイーチャンネル(TopSE Channel)

ソフトウェア開発者のための学習サイト「開発深知」については、開発深知とはをご覧ください。