形式手法入門講座

形式手法入門講座

本講座では、例題を用いながら、形式手法の種類と各々における形式化の考え方を理解していただきます。また、形式検証・証明の目的、実施概要や形式手法における段階的洗練の考え方、オブジェクト指向と形式手法の各特長、相互補完の考え方も合わせて学んでいきます。
本講座は、形式手法とは何かを知りたい方にとって最適なコースとなっています。

1日間～2日間

10:00　～　17:00

525,000円 ～ 1,050,000円 ※想定受講者数20名。受講者数が20名を超える場合は費用が変わります。

• 形式手法に関心のある方

• 特になし。

• 形式手法の種類と各々における形式化の考え方を体得し、人に説明できる。
• 形式検証・証明の目的、実施概要を体得し、人に説明できる。
• 形式手法における段階的洗練の考え方を人に説明できる。
• オブジェクト指向と形式手法の各特長、相互補完の考え方・現状を人に説明できる。

我々は、ソフトウェアエンジニアであれば形式手法は勉強すべき or 勉強する価値のあるものと考えています。形式手法は、VDM++やZ++といった名前からも推察できるように、オブジェクト指向と相互補完的です。また形式手法の考え方は、一般の仕様作成でも大いに参考になり、仕様の質を向上させてくれるはずです。そしてなにより形式手法はとても楽しいものです。
形式手法に関心をお持ちの方、豆蔵の講座で形式手法の扉を開けてみませんか！

１．はじめに
２．形式手法概観
　　 1) 形式手法の背景/課題とするところ
　　 2) 形式手法とは
　　 3) 形式手法の起源
　　 4) 形式手法発展の歴史
　　 5) 形式手法の種類と代表的手法
　　 6) “形式”とは
　　 7) 形式手法の範囲
３．集合や関数の基本知識
　　 1) 命題
　　 2) 述語
　　 3) 集合
　　 4) べき集合
　　 5) 直積
　　 6) 関係
　　 7) 関数
　　 8) 列
４． 形式仕様記述
　　 1) モデル指向型
　　 2) プロパティ指向型／代数型
　　 3) プロセス型
５．形式検証・証明
　　 1) 証明とはなにか
　　 2) 証明の対象
　　 3) 証明の基本的な構造
　　 4) ホーアの表明
　　 5) ダイクストラの最弱事前条件
　　 6) モデル指向型における証明の観点
　　 7) 代数型仕様における検証の観点
　　 8) 自動化について
６． 段階的な詳細化
　　 1) 段階的詳細化とは
　　 2) モデル指向型における詳細化
　　 3) 代数型における詳細化
７．モデル検査
　　 1) モデル検査とは
　　 2) 到達性解析
　　 3) 進行性解析
　　 4) 並行プロセスの遷移図表現
　　 5) 時相論理での性質記述
　　 6) 時相論理とは
　　 7) SPINの時相論理表明の判定
８．形式手法の適用事例
　　 1) 古典的な事例
　　 2) 国内の事例一覧
　　 3) その他事例一覧
　　 4) やや詳細な事例紹介
　　 5) 規格等
９．LFM（Light Formal Methods）
１０．形式手法の活用に向けて
　　 1) 形式手法がもたらす効果とその構造
　　 2) 形式手法の適用レベル
　　 3) オブジェクト指向と形式手法
　　 4) 参考：Correctness by Construction