VDMを用いた仕様記述・検証 〜 仕様検証編 〜：誰でも使える形式手法（5）（1/3 ページ）

　前回「VDMを用いた仕様記述・検証 〜 仕様記述編 〜」では、UMLで表現したモデル（連載第3回）をVDMで記述する過程を解説しました。今回は、前回記述したVDM仕様を基に仕様の検証を行います。

　VDMは記述した仕様を動作させてテストすることが可能です。仕様を検証するということに対して、

• 仕様がテストできると何がうれしいのか？
• 仕様の検証はレビューだけでよいのか？
• 記述した仕様は要求を満たしているのか？

などに疑問を持たれている方は、ぜひ本稿を一読して、“仕様を検証する”ということをあらためて考えてみてはいかがでしょうか？

仕様を検証するということ

　「仕様の検証」には以下の2つの側面があります。

• 正当性確認（Verification）
• 妥当性確認（Validation）

　これを仕様の検証に絞っていいますと、正当性確認は『記述した仕様が正しいことの確認』、妥当性確認は『仕様が要求を満たしているかの確認』といえます。この2つは、どちらか1つを満足するだけでは仕様として不十分で、両方が満たされている必要があります。

　仕様は要求と設計以降とをつなぐとても重要なものです。仕様に抜け・モレがあり不明確・不正確では、いくら優れた技術力をもってしても、ユーザーや顧客が満足するシステムは作れません。

　では、仕様の正当性や妥当性を検証するために、皆さんはどのような手法を用いて、どこまで検証をしていますか？

　ここでは「レビュー」「テスト」「証明」の3種類の検証方法を取り上げ、それぞれのメリット・デメリットについて見ていきます。

レビュー

　レビューは仕様の検証手段のみならず、システム開発においてとてもよく使われる検証方法です。恐らく読者の皆さんも日夜仕様書のレビューを行っているのではないでしょうか。

　レビューは、どこまで検証するのかを広い範囲で調節できます。例えば、綿密なレビューをするために入念な準備をし、明確にレビュー観点を決めたうえでレビューをすることもあれば、レビューを行ったという証拠が残せればよいといった“形だけのレビュー”を実施することもあります。このようにレビューと一口にいっても、実にさまざまな粒度のレビューを行うことができます。

　続いて、レビューの問題を2つ紹介します。

• レビュー品質がレビューアに依存しがちである
• 検証モレや検証し切れない部分が残る

　これらの原因はレビューという検証方法が人手でなされるところにあります。人間は、意味的矛盾に対する気付きに関しては非常に優秀ですが、網羅的に全体を見渡す、例えば、用語統一をするなどには弱いものです。そのため、どうしても検証が不十分になりがちです。

　では、レビューは検証方法として使えないということでしょうか？

　そんなことはありません。仕様には、人間の動機のように機械的に検証できないような部分があります。ですから、レビューを実施することはとても重要です。レビューは、それ単体だけでなく、ほかの検証方法と組み合わせて使うことにより、仕様の品質を向上させることが可能です。

テスト

　ここでいう仕様のテストは、テストケースに応じて、仕様を「動作させて」機械的に検証することです。その意味では、仕様の検証方法としてテストをしている方は非常に少ないと思います。なぜ少ないかというと、「機械的」に検証しようと思うのであれば、何かしら構文や意味が統一された表現方法を使わなければならないからです。VDMは、前回までの内容のとおり、構文や意味定義を持った言語を使って仕様を記述します。そのため、仕様を「テスト」できるのです。

　仕様をテストによって検証することは、レビューに比べればはるかに網羅性があり、正確です。しかし、次に説明する“証明”に比べれば網羅性に劣る部分があります。それは、テストケースの不足による検証モレがあり得るからです。この課題については、テスト工学の技術を使ってテストケースを検討することで、テストケース不足による検証モレを防ぐことができます。

　また、テストのいいところは、仕様変更や追加に強いことです。これは、同じテストケースを使って繰り返しテストをする「回帰テスト」が可能だからです。例えば、仕様変更や追加があったときに、仕様変更前と同じテストケースを使って仕様変更後の仕様をテストすることにより、仕様変更の前後でどこかに影響があるのか／ないのかを明確に確認できます。システム開発、特に組み込み開発での仕様変更や追加は日常茶飯事ですので、この仕様変更や追加に強いというメリットは、開発現場で実際に使うときに大きな要素となります。

証明

　証明は検証方法として最も正確で完全なものです。記述した仕様全体を証明できれば、その仕様は数学的に正しいことが保証されます。もし、完全な検証を求めるのであれば、検証方法として証明が最適でしょう。

　しかし、証明には以下のようなデメリットもあります。

• コストが掛かること
• 仕様変更に弱いこと

　まずコストが掛かる理由は、現在の技術ではすべての仕様を機械的に証明できず、どうしても人手による証明が必要になるからです。また、人手による証明は専門家の存在が不可欠であるため、それもコストが掛かる要因の1つといえます。

　2つ目の仕様変更に弱いというのは、テストのように回帰的に検証できず、仕様のどこかを変更・追加した場合は、すべてを証明し直さなければ「仕様が証明されている」という状態を保てないからです。これもやはりコストが掛かりますし、現実的ではありません。もし検証方法に証明を採用するのであれば、仕様を事前にしっかりと決めることと、仕様全体ではなく一部の品質が問われる部分に採用することです。