『ソフトウェア工学の道具としての形式手法』
2007年
歴史的な発展の流れを加味しながら、2007年現在の視点で形式手法の概要を解説
1. はじめに
2. 形式手法の現在像
形式手法の究極の目標
正しいシステムだけを系統的に開発
抽象的な記述から徐々に具体的なプログラム形式に変換する
この変換は正しいことが保証されている
Reasoning
表現力か解析能力のトレードオフ
3. 形式手法を鳥瞰
7つの観点
構造化設計
データ構造の定義、関数の機能仕様
静的な情報構造
クラス図、ER図など情報間の静的な関係の表現
振舞い仕様
ステート図など制御の流れなどの表現
リアルタイム性
時間的な特性が振舞いに影響を与える表現
プログラム検査あるいは検証
プログラムが要求仕様を満たすかどうかを検査
検証エンジン
特定の論理系に基づく表現ならびに推論機構を提供する
理論あるいは計算モデル
特定の基礎理論が提供する概念を直接表現できる