形式手法とモデリング - AlloyAnalyzerを中心に

1. 初めにソフトウエアの欠陥がもたらす影響がクリティカルになるにつれて、より間違いの少ない開発手法に注目が集まっています。そんな中で注目されている技術の1つが、形式手法です。形式手法とは、数学をベースにしたシステム開発手法の総称です。ですが、従来の形式手法は、数学の専門知識が必要だったほか、大がか

小林健一

2010年9月22日 20:00

1. 初めに

ソフトウエアの欠陥がもたらす影響がクリティカルになるにつれて、より間違いの少ない開発手法に注目が集まっています。

そんな中で注目されている技術の1つが、形式手法です。形式手法とは、数学をベースにしたシステム開発手法の総称です。

ですが、従来の形式手法は、数学の専門知識が必要だったほか、大がかりなシステム開発体制とあわせて語られることがほとんどでした。このため、一般の開発者にとっては、なじみのない技術でした。

こうした状況が、ここ数年で一変しました。PCの性能向上と、より使いやすいツールの提供により、誰でも簡単に試すことがのできる環境が整いつつあります。

本記事では、形式手法ツールの1つ「Alloy Analyzer」を取り上げ、以下の2つのポイントを中心に解説します。

形式手法は、導入の難しさが解消されてきている
形式手法は、ほかの現行の開発手法を補うかたちで利用できる

1.1. なぜAlloy Analyzerが開発されたのか

「ソフトウエアの欠陥を除去する」ことを考える際に、まず考えるのは、ソフトウエア・テストを行うことでしょう。ですが、ご存じの通り、テストではソフトウエアの欠陥を完全に排除することはできません。

「テストでは、欠陥が無いことは保証できない」（Edsger W. Dijkstra）

テストでは、特定の条件を入力した際の結果を確認します。つまり、テスト・ケースには"抜け漏れ"の危険が付きまといます。この問題を解決するため、形式手法では、仕様を数学的に記述し、これを証明しようとします。この証明を人力で行うのは限界があるので、これらを自動化する技術として自動定理証明やモデル検査といった技術が研究されています。これらの技術は自動ですべての条件や状態を洗い出すので、テストと比較して完全性が保証されるというメリットがあります。

ですが、こういった自動化技術にも弱点があります。例えば、モデル検査では、与えられたモデルを基にすべての状態を網羅するため、膨大なコストがかかるのです。この"状態爆発"という現象は、最新の計算環境をもってしても解決が難しい問題です。

ここで、Alloy Analyzerの開発者であるDaniel Jacksonは、1つの仮説を打ち出しました。

「Small Scope Hypothesis」（ほとんどの欠陥は、小さい探索範囲であっても反例として発見される）

すべてを網羅的に検証するのでなく、最も欠陥が発生しやすいところを集中的に検証すべき、ということです。Daniel Jacksonは、この考え方にのっとった形式手法を「Lightweight Formal Methods」と呼んでいます。

完全な証明よりも、現実的なコストの範囲内での欠陥の発見を目指すのです。Alloy Analyzerは、Lightweight Formal Methodsの考え方に基付いた形式手法ツールの1つです。

1.2. どういうことができるのか

Alloy Analyzerは、以下の特徴を持っています。

集合論と述語論理を理論基盤に持つ
与えられた仕様に対し、指定したプロパティを満たす例を探すことができる（述語の検証）
与えられた仕様に対し、指定したプロパティを満たさない反例を探すことができる（表明の検証）

上記の例と反例の探索が、Alloy Analyzerを使って設計を行う際に、非常に役立ちます。通常、クラス図やデータ・モデルを作成した際のレビューは、手作業で行うことが多いかと思います。Alloy Analyzerの場合、データ構造を表す仕様を手軽に記述できるため、クラス図の多重度の間違いや、複数の制約条件の組み合わせの結果を、その場で確認することができます。