ライトウェイトな形式手法で高品質な仕様をこの手に！：誰でも使える形式手法（1）（1/3 ページ）

仕様の“不確かさ”が原因で痛い目を見た。そんな経験をお持ちの皆さん、この機会に形式手法をマスターし、高品質な仕様を作成してみませんか。

[植木雅幸（CSK），＠IT MONOist]

　近年、組み込みソフトウェアは高機能・多機能化により複雑さを増し、開発規模が著しく増大しています。

　こうした厳しい状況の中、ソフトウェア開発の現場では、以下のような問題に直面するケースが多く見られます。

• 出荷前に仕様の不具合が発見され、対応に追われた
• 修正をしたら思わぬ個所に不具合が発生した
• 外部に依頼したソフトウェアの品質がなかなか上がらない
• ソースコードしかなく、仕様書が残っていないため、どこを修正すればよいのか分からない
• 仕様をレビューすることの限界を感じる

　では、なぜこのような問題が起こるのでしょうか？ その原因の1つは“仕様の不確かさ”にあります。読者の皆さんの中にも、『仕様（の不確かさ）が原因で痛い目を見た』という経験をお持ちの方がたくさんいらっしゃるのではないでしょうか？

　そこで本連載では、“不確か”な仕様を“厳密”にする「形式手法（Formal Methods）」の1つである『VDM（Vienna Development Method）』を取り上げ、実際の利用方法を示しながら、形式手法が持つ「厳密性」と「信頼性」の向上効果を読者の皆さんにお伝えしたいと思います。「なんだか難しそうだなぁ」「実際に現場で運用できるものなの？」と不安や疑問を感じるかもしれません。しかし、形式手法は決して難しいモノではありません。前述したような問題でお困りであれば、形式手法にチャレンジする価値が十分にあると筆者は考えます。

　本連載では、以下の2つの観点で解説を進めていきます。

• 形式手法を用いて仕様を記述する
• 開発プロセス中で形式手法を使う

　まず、連載第1回となる今回で、形式手法の使い方を理解するに当たっての前提知識「『形式手法』とは何か？ 『VDM』とは何か？」について触れたいと思います。

	関連リンク：
⇒	いまさら聞けない 形式手法入門

数学が基礎!? 形式手法とは

　形式手法とは、数学をベースに1970年代ごろ欧州で生まれた開発手法のことで、集合論や論理学の考え方を基に、システムやソフトウェアの「仕様」を正確かつ詳細に記述・検証することを核とし、モデル化や検証などの技術を含んだ包括的な手法です。ちなみに現在、百種類ほどの形式手法が存在します。

　従来の自然言語や、UML（Unified Modeling Language）などの図式表現で記述した仕様では、“あいまいさ”や“解釈の違い”を完全に排除することが難しく、記述した仕様の正しさを検証する手段も（一般的に）レビューに頼るしかありません。

　これに対して、形式手法は1つの手法に対して1つ以上の「仕様記述言語」を持ちます。この仕様記述言語が数学を基盤とした厳密な仕様記述を可能にします。また、前述したように形式手法は包括的な手法ですので、仕様記述言語で記述した仕様を「検証」する技術も備えています。明確な意味定義を持つ言語で記述しますので、仕様の正しさを機械的に検証するための支援が可能です。

　また、従来の手法（自然言語）で記述された仕様に対する不具合の多くは、「要件定義工程」ではなく下流の「テスト工程」で発見されるため、修正のために手戻りが発生するなど、そのコストは計りしれません。一方、形式手法では、仕様レベルで不具合を検証・修正するため、従来の手法に比べて不具合を早期に検出できますので、結果的に修正コストを抑えられるといったメリットがあります。

形式手法の分類〜 記述手法とモデル検査 〜

　次に、形式手法の分類について説明します。図1のように形式手法には大きく分けて2種類の手法が存在します。1つは「仕様を正確に記述することに特化した“記述手法”」。もう1つは「システムの振る舞い仕様を検証する“モデル検査”」です。

図1　形式手法の種類

記述手法

　記述手法はさらに「性質規範型（代数仕様）」と「モデル規範型」の2つに分類されます。

• 性質規範型　
  性質規範型の形式手法は「代数仕様」とも呼ばれ、システムを外部から見てその性質を公理や抽象データ型を用いて表現します。代表的な手法には「CafeOBJ」や「Maude」があります。性質規範型は代数を基礎とする分、多少ハードルが高いといえるでしょう。
• モデル規範型　
  モデル規範型の形式手法には、本連載の題材である「VDM」をはじめ、「Z記法」「Bメソッド」といった手法があります。これらはシステムをその内部から見て、内部構造の構成的定義をデータや操作を用いて行います。また、基礎となる学問は集合論や一階述語論理です。モデル規範型は、比較的プログラム言語に近い考え方を持っているため、現場で使いやすい手法といえるでしょう。

モデル検査

　モデル検査は近年注目されている手法の1つで、ソフトウェアの振る舞い仕様に対して、可能な実行パターンを網羅的かつ自動的に検査することにより検証を行う手法です。モデル検査の代表的な手法には「Spin」や「LTSA」「SMV」があり、主に開発プロセスの「設計工程」において、状態遷移やメッセージ通信の中でプロセスがデッドロックやライブロックを起こさないことを網羅的に検証します。そのため、特に品質が要求される部分や複雑な状態遷移の正しさを検証することに向いています。

　これらの手法には当然得意、不得意な分野があります。対象のシステムや検証したい性質によって、使い分けたり一緒に使ったりすることをお勧めします。

ライトウェイトな形式手法

　形式手法、特に記述手法には2種類の使い方があります。

　1つ目は形式手法の本来の目的、究極の方法ともいえる「Correctness by Construction」と呼ばれる使い方です。これは、形式手法に示されている手順に従って、要求から仕様、設計へと記述を行い、それらの間の正しさをすべて『証明』するものです。また、「要求」→「仕様」→「設計」と変遷していく中でリファインメントと証明を繰り返し、正しさが証明された記述から最終的に正しさが保証された変換方法によってプログラムを生成します。このリファインメントと証明によってシステム開発の全工程を正しく開発できます。

　しかし、このCorrectness by Constructionは、開発プロセスの上流工程に多大な影響を与える可能性が高いため、開発現場でいきなり使う（導入する）には障壁が高く、使用する際はかなりチャレンジングな覚悟が必要となります。

　また、Correctness by Constructionはすべてのモデルが証明されている必要があります。まさに“究極”の方法ですね。しかし、現場で実際に使うことを考えたときに、果たしてすべての仕様に証明が必要でしょうか？ 証明まで行って品質を確保しなければならないような仕様は、システムのごく一部だけであることは往々にしてあります……。

　こうした“ハードルの高さ”を軽減させる（形式手法を“ライトウェイトに使う”）ために登場したのが、「ライトウェイト形式手法」です。ライトウェイト形式手法では仕様を形式仕様記述言語を用いて厳密に記述し、その仕様を証明ではなく『テスティングによって検証』を行います。ライトウェイト形式手法は形式手法が持つ「記述力」と「検証力」のバランスを兼ね備えているため、現場での導入も比較的容易に行えます。

　さらに、仕様の検証をテスティングで行うことによるメリットもあります。その1つが、従来のテスティング手法のノウハウを応用した「仕様の回帰テスト」が可能な点です。一度、仕様とテストケースの記述を行ってしまえば、仕様レベルで自動的に繰り返しテストを行うことができます。また、開発プロセスにおいては、仕様の段階で作成したテストケースを下流工程での検証材料として使うことができる、といったメリットもあります。

　本連載で紹介するVDMは、“ライトウェイト形式手法の考え方”を実践しやすい手法です。では、VDMとは具体的にどのような手法なのでしょうか？ 次ページで詳しく見ていきましょう。