モデル検査事例演習(全18回)

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

講義概要

本講座は、モデル検査の実務を想定し、その開始から終了までの全プロセスを意識した演習を行います。モデル検査とは、形式手法とはといった基本的な事項から解説し、モデル検査入門としてもご覧いただけます。
講義は、動画と小テストの構成になっております。

講義は、こちらから登録することができます。
モデル検査事例演習 | 開発深知

01_モデル検査事例演習

本講義の構成

02_本講義の構成

第1回:モデル検査とは
モデル検査、形式手法、ソフトウェア品質監査制度、モデル、検査式、不具合が見つかる原理、反例、モデル検査の課題と対策について解説します。
第2回:モデル検査のデモ
モーター監視プログラムのデモ(システムの概要、出荷前の試験で不具合発生)を例に、モデル検査を用いて不具合解析(作成したモデル、検査結果、反例の解析)について解説します。
第3回:モデルのコーディング
例題を元に変数、状態遷移図の作成についてモデル検査器のSMVを元に解説してきます。また利用可能な演算子、演算子の優先順について取り上げます。
第4回:例題とCTL式
タスクの優先度と排他制御のシステムの例題を元に、変数の抽出、変数の値の決定、仕様から状態遷移図の作成、モデル作成(状態遷移図をコーディング)、SMV系のモデル検査器で用いる検査式CTL(Computation Tree Logic)について解説します。
第5回:演習問題
多重割り込みシステム、小型船舶用簡易無線機の課題について解説します。
第6回:事例演習概要
実際のシステムを題材とした事例演習について解説します。
第7回:モデル検査の適用プロセス
モデル検査の適用プロセス、プロセスの必要性、モデル検査報告書、検査計画の策定、適用方針の立案、モデル化の方針立案、検査項目の方針立案、検査対象の絞込みと抽象化、モデル設計、モデルの妥当性検査、本検査、結果解析、適用審査、報告書の記載内容とフォーマットについて解説します。
第8回:仕様調査・不具合調査(検査計画の立案)
仕様調査(仕様書の題材)、CSRSシステム仕様書、CSRSシステムの仕様の例、不具合調査(ソースコードの題材)、電子掲示板プログラム、依頼事項、報告書の例について解説します。
第9回:モデル検査の方針立案
適用方針(目的、適用条件)、モデル化の方針、検査項目の方針、依頼元との合意、デッドロックは悪いプログラムか?について解説してきます。
第10回:検査対象の絞込みと抽象化
絞込み、抽象化、理論状態数と到達可能状態数及び抽象化の例について解説します。
第11回:モデル設計
自然言語からのモデル化(具現化、変数と値の割り当て、状態遷移表や図)、ソースコードからのモデル化(基本手法、フローチャート→SMVコード、PC(プログラムカウンター)省略、PC省略を奨励しない例)、報告書への記載について解説していきます。
第12回:モデル&CTL式製作 妥当性検証
モデルのコーディング(フォーマットの制定、変数名、よくあるミス)、モデルの妥当性検査、検査項目の意義、CTL式のコーディング、予備検査が必要な例について解説していきます。
第13回:ラベル付けアルゴリズム(基本_1)
CTLのラベル付けアルゴリズム、AG(P)のラベル付けアルゴリズム、A[P U Q]のラベル付けアルゴリズムについて解説します。
第14回:ラベル付けアルゴリズム(基本_2)
EG(P)のラベル付けアルゴリズム、EF(P)のラベル付けアルゴリズム、E[P U Q]のラベル付けアルゴリズム、早見表(基本の8つのパターン)について解説します。
第15回:ラベル付けアルゴリズム(応用)
入れ子構造となったCTLのラベル付けアルゴリズムについて解説します。
第16回:CTLに関する諸規則
CTLの諸規則(CTLの真偽の相互関係、CTLの変換、CTLと否定(!)の関係)について解説します。
第17回:本検査と結果解析
モデル検査実行(検査器について、Cadence SMVについて)、反例解析について解説します。
第18回:報告書作成と成果のPR
モデル検査報告書の例と成果のPRについて解説します。

講師

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

小テストの例

本講義では、各講義動画と合わせて小テストを設定しております。小テストの解答については、モデル検査事例演習 | 開発深知 の講義でご確認ください。
スクリーンショット 2015-03-30 11.40.26

本講義について

03_本講義について

目標:組織におけるモデル検査推進者の育成
・業務としてモデル検査を適用する
・成果をアピールして、組織内での本格導入を推進する
形態:演習開始(第6回)からはシミュレーション
・受講生が車内の他の技術者からモデル検査の適用を依頼された
・演習課題は実際のソフトウェア製品に基づいた題材

講義スライド

モデル検査事例演習の講義からスライドをピックアップしてご紹介します。

ソフトウェア品質監査制度

04_ソフトウェア品質監査制度
ソフトウェア品質監査制度
2010年3月 経産省産業構造審議会分科会情報システム・ソフトウェア小委員会
第三者による検証・妥当性確認のフレームワークの必要性」から

モデル検査とは?(第1回)

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

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

代表的な3つの手法
 形式仕様記述(VDM、Z、Bなど)
モデル検査
 SMV、SPINなど
定理証明
 Agda、Coqなど

本講座「SMV(Symbolic Model Velifier)」を用いる

モデルとは?(第1回)

06_モデルとは?

モデルとは?
 仕様書/ソースコードをモデル検査器毎の専用言語で記述したもの

検査式とは?

07_検査式とは?

検査式とは?
 検査したい性質を論理式(CTL式)で記述したもの

反例とは?(第1回)

08_反例とは?

反例とは?
 不具合に至るまでの経路(パス:時系列な変数の値の変化)

モデル検査を用いて不具合解析(第2回)

01_モデル検査を用いて不具合解析

(1)モデル化
ソースコードからモデルを作成する。→ソースコード紹介
(2)検査方針
「不具合の状況が発生しないはず」を検査すれば良い。
 →本当に不具合が発生するなら反例でそのパスが出力される
検査項目
加速オフで減速オンで表示が加速中となり続けることはないはず

CTL式 !EF(EG(Kasoku = 0 & Gensoku = 1 & Hyouji = 1))

検査結果(第2回)

02_検査結果

反例の解析(第2回)

03_反例の解析
デモではExcelで整理(モデル検査器の画面でも良い)

状態遷移図=有限個の状態+遷移関係(第3回)

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

状態遷移図は(第4回)

14610302_状態遷移図は

(1)変数を抽出して、変数が取り得る値を決定する(第4回)

14610401_(1)変数を抽出して、変数が取り得る値を決定する

(2)仕様を読みながら「変数毎の状態遷移図」を作成する(第4回)

14610402_(2)仕様を読みながら「変数毎の状態遷移図」を作成する

(3)モデル作成(状態遷移図をコーディングする)

14610403_(3)モデル作成(状態遷移図をコーディングする)

講義は、こちらから登録することができます。
モデル検査事例演習 | 開発深知
また、動画をご覧になる場合には、開発深知の会員登録(無料)が必要です。
開発深知登録方法について | 開発深知ブログ

関連講義

モデル検査事例演習の関連講義について紹介します。

性能モデル検証
本講座では、ネットワーク家電の制御ソフトウェアを題材とした産業ソフトウェアの性能モデル検証問題を扱う。設計モデルの性能面に関する動作の正しさを自動的に検証する性能モデル検査ツールUPPAALを使用し、実際のシステム開発に適用する方法を習得する。
SMV入門
本講義は、モデル検査器SMVを用いて専用言語であるSMV言語の文法の習得、検査式の作成方法の習得、モデル検査器SMVの操作方法の習得を目指します。
VDM、SPINから始める形式手法入門
本講義では形式手法の概要から説明し、VDMやSPINなどのツールの使い方などについて解説していきます。
形式仕様記述(セキュリティ編)
本講座では、最初にアクセス制御ポリシを強制するセキュリティ機構の段階的詳細化に基づく構築について、Event-Bを使い、ポリシを強制するセキュリティ機構を段階的詳細化を使って構築する過程について学びます。またセキュアプロトコルへの検証応用等、モデル検査技術のセキュリティ分野への応用を解説します。
ソフトウェア工学入門
本講座においては、ソフトウェア開発プロセス、UML、要求工学、設計法、形式手法に関してその位置づけと基礎知識、特に解決しようとする課題と解決に向けた基本的な考え方を習得していきます。
クラウド実践
本講座では、クラウドコンピューティング環境上での分散アプリケーション開発手法を扱います(トップエスーのクラウド入門に相当)。
設計モデル検証(基礎)
講義では、ソフトウェア開発における検証について解説している講義です。モデル検査とテストの違い、モデル検査ツールSPIN、設計・検証プロセス、フレームワーク・テンプレートの作成、デバッグと検証などについて解説します。
形式仕様記述(基礎)
本講座では、形式仕様言語を用いた開発対象のモデル化の問題を扱います。多様なモデルの中で、特に静的な情報構造にまとを絞り、形式手法を用いた系統的な開発の方法を学習します。
実装モデル検証
本講座ではJML(Java Modeling Language)をテーマに、Design By Contract(契約に基づく設計)の手段としてJML、単体テストの手段としてのJML、プログラムの静的検証とJMLについて解説します。
設計モデル検証(応用)
本講座では、代表的な3つのモデル検査ツールであるSPIN、SMV、およびLTSAを通して、ソフトウェア設計検証の難しさを体感した上で、設計モデルの特徴に合わせたモデル検査ツールの使い分け、およびノウハウを習得していきます。
MindStormで学ぶ、UPPAALによる時間制約の検証
時間制約を扱えるモデル検査ツールUPPAALを使って、時間に関する情報をUPPAALでモデル化し、時間制約を検証する手法について解説します。
並行システムの検証と実装
本講座では、信頼性の高い並行システムを構築することを目的として、CSP, FDR, JCSPを軸に、CSPによる並行システムのモデル化、FDRによる検証、JCSPによる実装方法について解説します。
モデル検査ツールを使った設計モデルの検証
本講義では、検証とは何かや、モデル検査とテストとの違い、検証の必要性、分散システムにおける検証について解説していきます。
基礎理論
形式手法を知る上で必要となる基礎知識について学んでいく講義です。形式手法入門としてもご覧いただけます。
SMVで学ぶモデル検査入門
モデル検査の概要、企業での取り組みやデモ、例題を交えながらモデル検査について解説します。
プロセス分析ツールPATによるモデリングとモデル検査
PAT(プロセス分析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)によるリアルタイム性のモデル検査の解説動画です。
プロセス分析ツールPATで学ぶ並行プロセスのモデル検査
並行プロセスの解析や検証ツールであるPAT(プロセス分析ツール)を用いた並行プロセスのモデル検査について解説します。

参考リンク

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

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