HOME>高度人材育成>CVS教程:対話型証明

CVS教程:対話型証明

概要

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

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

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

▲ページ先頭へ

対話型証明コース概要

対話型証明とは、システムに期待する性質を「定理」とみなし、形式的に推論を積み重ねて定理の「証明」を構成することで、システムに不具合がないことを保証する手法です。

本コースでは,システム開発の技術者・マネージャを対象として、Agda を使った対話型証明を初歩から学びます。

・関数による形式モデリング(三日間)

検査対象であるプログラムやシステムの仕様・設計を Agda 言語を用いて書き下し、不整合や曖昧性のない記述を得る技術を学びます。

内容: 関数と型による記述、支援系 Agda の機能、Agda 言語の紹介、システムの記述例、仕様の形式的な記述演習

・形式モデルの証明(準備中)

プログラムなどの検査対象に加え、論理体系を Agda 言語の上に実装し、プログラムの持つ性質に証明を与えるための知識と技術を学びます。
内容: 論理式と推論,命題論理,Agda による証明の構築,述語論理,論理式による性質の表現とその証明例

▲ページ先頭へ

研修コースパッケージ

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

▲ページ先頭へ