CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コース ・ニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

CVS教程

科学技術の進歩に伴い、情報処理システムはますます複雑になり、遍在化しています。そのためシステムの信頼性が厳しく要求され、システムの検証技術への要求と期待がますます高まってきています。

それらの期待に応える技術の一つとして、近年数理的技法(形式手法)が脚光を浴びています。数理的技法は数学や論理を使って厳密な検証を行うので、従来のテストやシュミレーションでは発見が困難な不具合を発見することができるからです。

しかし、現在、数理的技法を日本語で学ぶ良い教材はありません。英語で書かれたものや大学での講義のための教材はいくつかありますが、論理学などの素養を持たないが数理的技法に興味を持つ技術者のための教材・教科書は見当たりません。

このような状況を打破するため、産業技術総合研究所システム検証研究センターではCVS教程と呼ばれる、数理的技法を学ぶための研修コース体系を構築し、その教材を開発いたします。

■CVS教程の開発方針

●「理論」と「対象」の両立
cvs course of study 数理的技法を正しく理解しうまく適用するには、その背後の論理学や数学的概念の正確な理解が不可欠です。一方抽象的で具体的な対象と結びつかない理論だけではやはり数理的技法を上手に適用することは出来ません。CVS教程では「理論」と「対象」の片方に偏ることなく両者を融合した形で扱い、正確かつ具体的な理解を目指します。

●「教材」と「教授法」の提供
受講者のための教材・教科書に加え、集団研修を行うときの留意点・解説法など教えるための材料も開発します。

●幅広い受講者対象
数理的技法や論理についてほとんど知識のない初学者から、問題にあわせて適用する数理的技法を選ぶ能力を持つエキスパートの養成まで、多様な受講者に対応できる教材の開発を目指します。

※システム検証研究センターでは、研修コースの開催運営は教材開発のための試行を除いて一切行いません。

■モデル検査研修コース

モデル検査法について学ぶコース。 NuSMVやSpinなどモデル検査ツールを使った演習を通じて研修を行いますが、どのようなモデル検査ツールでも適用できるよう、モデル検査の原理的理解を 与えることを目標とします。

course system ●初級:論理学・数理的技法の知識を仮定せず、モデル検査の概要を学び、作業手順を身につけるためのコース。
モデル検査研修コース初級編の教科書が出版されました。

●中級:初級修了程度の知識を仮定して、モデル検査で使われる標準的なテクニックや運用方法を学ぶコース(開発終了)
モデルの作り方に関する技術(モデルの合成、モデルの抽象化)、CTL検査式の概要を説明します。

●上級:中級修了程度の知識を仮定して、モデル検査ツールの動作原理やより進んだ適用技術を学ぶコース(開発中)
検査アルゴリズムや時相論理、検査効率のよいモデルの作り方などを扱います。

■対話型検証研修コース

対話型検証法について学ぶコース。
Agda、Coq、Isabelleなどの対話型検証ツールを使った演習を通じて研修を行いますが、どのような定理証明ツールでも適用できるよう、対話型検証の原理的理解を与えることを目標とします。

●初級:論理学・数理的技法の知識を仮定せず、対話型検証の概要を学び、作業手順を身につけるコース(開発中)

●中級:初級修了程度の知識を仮定して、対話型検証で行われる標準的なテクニックや運用方法を学ぶコース(開発中)
-データを記述するためのコース
-入力出力型プログラムの検証
などを企画開発中

●上級:中級修了程度の知識を仮定して、対話型検証ツールの動作原理や、より進んだ適用技術を学ぶコース(開発中)
-型理論
-証明の検査アルゴリズム
などを企画開発中

■準備コース

中級〜上級のコースの前に、初級〜中級の復習を短時間で行うコースや、論理の基礎(命題論理・述語論理・文法と意味など)を学べるコースも開発中。

産総研ホーム > 組織 > 研究センター > システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.