『ソフトウェア工学の道具としての形式手法』

2007年

歴史的な発展の流れを加味しながら、2007年現在の視点で形式手法の概要を解説

1. はじめに

2. 形式手法の現在像

形式手法の究極の目標

正しいシステムだけを系統的に開発

抽象的な記述から徐々に具体的なプログラム形式に変換する

この変換は正しいことが保証されている

Reasoning

表現力か解析能力のトレードオフ

3. 形式手法を鳥瞰

7つの観点

構造化設計

データ構造の定義、関数の機能仕様

静的な情報構造

クラス図、ER図など情報間の静的な関係の表現

振舞い仕様

ステート図など制御の流れなどの表現

リアルタイム性

時間的な特性が振舞いに影響を与える表現

プログラム検査あるいは検証

プログラムが要求仕様を満たすかどうかを検査

検証エンジン

特定の論理系に基づく表現ならびに推論機構を提供する

理論あるいは計算モデル

特定の基礎理論が提供する概念を直接表現できる