SMVで学ぶモデル検査入門(全3講義)

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

講義概要

本セミナーでは、モデル検査の概要に加えて、企業での取り組みやデモ、多くの例題を交えながら初心者の方にも分かりやすく説明します。また、演習問題も用意していますので、実際にモデル検査ツールSMVを操作することで、より深い理解を得ることができます。

※このビデオは、2011年5月26日(木)に行われました、トップエスイー教育センターのセミナーを別撮りしたものです。

講義は、下記ページから登録することができます。
SMVで学ぶモデル検査入門 | 開発深知
また、動画をご覧になる場合には、開発深知の会員登録(無料)が必要です。
開発深知登録方法について | 開発深知ブログ

講義構成

全3講義の動画の構成は以下の通りです。

その1:モデル検査とは
モデル検査とは何かについてデモを交えながら不具合解析やモデル検査のWebサービスなどについて解説します。
その2:SMVへの出力等
SMVへの出力(変数毎の状態遷移図)等について解説していきます。
その3:課題と解説
課題とその解答例について解説していきます。

01_構成

講義の構成は以下の通りです。

第1部:【概要】
1. モデル検査とは?
2. 企業での普及活動
3. モデル検査Webサービスの紹介
第2部:【講習】
1. モデル検査器
2. モデルとは
3. 状態遷移図
4. 例題1
5. 例題2
6. 例題3
7. 変数毎の状態遷移図
8. 例題4
9. 検査項目(検査式)
10. 例題4の検査式
11. モデルの修正 → 再検査
第3部:【演習課題】

講義開始日

2016年3月16日

講師

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

講義スライド

SMVで学ぶモデル検査入門の講義スライドをピックアップして紹介します。

モデル検査とは?

02_モデル検査とは?
形式手法(数理的技法)の1つ

形式手法とは→特定の手法を指すわけではない
 →数学・論理学を基盤としたシステムの記述方法や検証手法の総称

代表的な3つの手法

  • 形式仕様記述(VDM, Z, B等)
  • モデル検査(SMV, SPIN等)
  • 定理証明(Agda等)

モデル検査Webサービスの紹介

03_モデル検査Webサービスの紹介
本システムのメリット

  • モデル検査器のインストール不要
     →PCへのSWのインストールを制限している企業には◎
  • ライセンス問題を考える必要がない
     →公開されていても「商用利用禁止」のモデル検査器もあるので注意要
  • 大容量メモリ(さつき)を利用できる
  • いつでもどこからでも手軽にモデル検査が利用できる
  • 64bit版モデル検査器を利用できる(本システムで初公開)
     →「64bit版+大容量メモリ」で状態爆発の回避に有効
  • 無料

モデル検査器

04_モデル検査器

SMV系(NuSMV, CadenceSMV, 64bit版モデル検査器)
→データ構造としてBDD(Binary Decision Diagram)を採用。
 大きな状態のモデルを検査することができる。
 モデル記述言語の構文が簡単で処理が高速。
SPIN
→モデル記述言語としてPromelaを採用。
 PromelaはC言語に似ているため取っ付きやすい。
UPPAAL
→画面上で状態遷移図の記述ができる。GUIが充実。
 状態遷移図からモデルを自動生成する機能がある。

本講習はSMV系
 →実業務に適用すると大きな状態のモデル検査が必須であるため。

教科書・参考書

モデル検査に関する書籍や講義・セミナーを紹介します。

モデル検査に関する書籍

モデル検査初級編: 基礎から実践まで4日で学べる
https://books.google.co.jp/books?id=aGV0QgAACAAJ&hl=ja
著者 産業技術総合研究所システム検証研究センター
出版社 ナノオプト・メディア, 2009
ISBN 4764955059, 9784764955059

モデル検査上級編: 実践のための三つの技法
https://books.google.co.jp/books?id=qPIIRAAACAAJ&hl=ja
著者 産業技術総合研究所システム検証研究センター
出版社 ナノオプト・メディア, 2010
ISBN 4764955067, 9784764955066

SPIN モデル検査: 検証モデリング技法
https://books.google.co.jp/books?id=cAahOgAACAAJ&hl=ja
著者 中島震
出版社 近代科学社, 2008
ISBN 4764903539, 9784764903531

モデル検査に関する講義・セミナー

05_モデル検査に関する書籍

関連講義

SMVで学ぶモデル検査入門の関連講義について紹介します。

SMV入門
モデル検査ツールSMVについて学習する講義です。講義は、動画と小テストの構成になっております。SMVの概要、SMVの種類、SMV専用言語の文法の種類、検査式について解説します。また状態線地図の概要、状態の数とパスの数、変数ごとの状態遷移図について例題などを通じて解説します。
VDM、SPINから始める形式手法入門
近年、ソフトウェア開発における効率的な信頼性向上のためのアプローチとして、形式手法が注目され話題になっています。「形式手法」とはアプローチの総称であり、実際の活用においては多様な手法・ツールから問題に適したものを選び、その活用方針を議論し定める必要があります。本講義では形式手法の概要からツールの使い方などについて解説していきます。
モデル検査ツールを使った設計モデルの検証
本講義では、検証とは何かや、モデル検査とテストとの違い、検証の必要性、分散システムにおける検証について解説していきます。
モデル検査ツールとは何かや、形式的検証手法であるモデル検査ツールの種類について紹介している講義で、モデル検証についての入門的な内容となっております。
モデル検査事例演習
本講座は、モデル検査の実務を想定し、その開始から終了までの全プロセスを意識した演習を行います。モデル検査、形式手法、ソフトウェア品質監査制度、モデル、検査式、不具合が見つかる原理、反例、モデル検査の課題と対策について解説します。
MindStormで学ぶ、UPPAALによる時間制約の検証
本チュートリアルでは,特に時間制約を扱えるモデル検査ツールUPPAALを使って検証する方法について解説します。前半では、時間に関する情報をUPPAALでモデル化し、時間制約を検証する手法の概要を説明します。また、本講義はUPPAALについてある程度知識のある方が対象となります。
設計モデル検証(基礎)
本講義では、ソフトウェア開発における検証について解説している講義です。モデル検査とテストの違い、モデル検査ツールSPIN、設計・検証プロセス、フレームワーク・テンプレートの作成、デバッグと検証などについて解説します。
形式仕様記述(基礎)
本講座では、形式仕様言語を用いた開発対象のモデル化の問題を扱います。本講座では、多様なモデルの中で、特に静的な情報構造にまとを絞り、形式手法を用いた系統的な開発の方法を学習します。
形式仕様記述(セキュリティ編)
本講座では、最初にアクセス制御ポリシを強制するセキュリティ機構の段階的詳細化に基づく構築について、Event-Bを使って学びます。Event-BはBメソッドを基盤として開発されたシステム開発手法で、イベントの概念が導入されている点に特徴があります。ここでは、ポリシを強制するセキュリティ機構を、段階的詳細化を使って構築する過程について学びます。
実装モデル検証
一般的なソフトウェア開発に利用できる「形式手法に基づくプログラム解析技術」としてのJML(Java Modeling Language)について学んでいきます。Design By Contract(契約に基づく設計)の手段としてJML、単体テストの手段としてのJML、プログラムの静的検証とJMLについて解説します。
性能モデル検証
本講座では、設計モデルとして、標準のモデル記述言語UML、特に性能面に関するモデル化を可能にするProfile for SPT (Schedulability, Performance, and Time)を採用して、入力モデルへの変換手法を習得していきます。さらに、実際に組込ボード上でのソフトウェア開発を通して、ソフトウェア設計検証の難しさを体感した上で、UPPAALツールの適用における難しさを解決するための検証プロセス、およびノウハウを習得でいます。また、グループ討議を通じた例題演習により、議論を通してモデル検査技術の理解を深め、検証プロセスの実用的ノウハウを体得できる効果が期待できます。

参考リンク

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

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