HOME>高度人材育成>CVS教程:モデル検査

CVS教程:モデル検査

概要

現在、ソフトウェアや情報処理システムは複雑で規模の大きなものとなり、開発の際に高い信頼性を保証することが難しくなってきています。というのも、多くの場合システムは限られたテストケースについてしか動作を確認できません。障害の原因となる、開発者の意図しないシステムの振る舞いは、システム稼動後に初めて発見されるのです。

このような問題に有効な技術が「数理的技法」(Formal Methods)です。 特に、システムの意図されていない振る舞いを発見することに大きな威力を持ちます。既に地下鉄の運行システム、原子力発電所の制御、通信プロトコルなど信頼性を求められる多くのシステム開発で活躍し、バグの発見と信頼性の向上に貢献しています。

産業技術総合研究所組込みシステム技術連携研究体では、企業におけるシステム開発に数理的技法を適用してきた経験をもとに、その知識と技術を伝える研修コースを開発しています。これらのコース体系を CVS 教程と呼んでいます。

▲ページ先頭へ

モデル検査コース概要

モデル検査とは、状態遷移系として表されるシステムを全数探索によって検査し、潜在的な不具合を発見する技法です。
本コースでは,システム開発の技術者・マネージャを対象として,モデル検査の初歩から高度な知識までを学びます.
研修コースダウンロード

初級編(四日間)

モデル検査の概要を理解し、典型的な検査ツールを使って一通りの検査を実行できるようになることを目的とするコースです。

・内容:

モデル検査の概要,ツール(NuSMV, Spin)を使った検査プロセス、排他制御問題への適用、線型時相論理式の解説,仕様書検証の演習

・テキスト:

モデル検査[初級編]
  • 著者:産総研システム検証研究センター
  • 発行:ナノオプト・メディア
  • 発売:近代科学社
  • ISBN:9784764955066

上級編(三日間)

モデル検査の典型的な技術を学び、独力で大きな問題に挑戦できる能力を身につけることを目的とするコースです。

・内容:

状態遷移系の合成(同期合成,非同期合成),プログラムのモデル化,状態遷移系の抽象化,計算木論理の解説

・テキスト:

モデル検査[上級編]
  • 著者:産総研システム検証研究センター
  • 発行:ナノオプト・メディア
  • 発売:近代科学社
  • ISBN:9784764955059

▲ページ先頭へ

研修コースパッケージ

教科書といったモデル検査を学ぶための資料に加え、モデル検査を教えるための資料を用意し、 パッケージ化しました。指導ノウハウと準備済みの演習環境によって研修開催の労力を軽減し、より広い知識伝達を可能にします。

▲ページ先頭へ