いまさら聞けない 形式手法入門：品質向上技術解説（2/3 ページ）

形式手法の必要性とメリット

　形式手法が古くから研究されてきた分野であると前述しましたが、なぜいまになって取り上げられているのでしょうか。

　海外では長い間、人工衛星や航空機、原子炉の制御といったミッションクリティカルなシステムにおいて形式手法が利用されてきました。もちろん今後も形式手法は欠かせない技術です。

自然言語におけるあいまいさ

　さて、皆さんはどのような仕様書を作成しているのでしょうか。CDプレーヤのディスク取り出し機能を例に、少し考えてみましょう。

　まず、「CDのEJECTボタンが押されたらCDを排出する」という仕様を書き、次に「再生中の場合は停止して」「停止中の場合は……」などと書いてだんだん条件が複雑化。文章だけでは分かりにくくなったので表を添付する、という感じでしょうか。ここまで書いて次は設計です。UMLで状態遷移図とシーケンス図を描いて、いよいよ実装に入ります。

　プログラマーは、「再生中とは何か」「シーク中は再生中か」を考えます。優秀なエンジニアは条件をまとめて仕様作成者とコミットするでしょう。人によってはそのような状態を考えずに実装します。結果として、製品の仕様に作成者たちも分からない状態ができてしまいます。私はいままでそういう現場を見てきました。

　では、形式手法ではない方法、つまり自然言語では厳密な仕様は記述できないのかというと、不可能ではないと思います。ただし、自然言語ではどのような記述も許されてしまい、一意に解釈できる記述を行うのは困難です。仮に自然言語で厳密な仕様を記述できたとしても、理解しにくい冗長な表現になってしまうでしょう。また、ルールのない記法において、仕様が正しいことを証明する手段はありません。

　自然言語で仕様を記述した場合、仕様自体にあいまいさが入り込む可能性が高く、第三者が開発・検証を行ったり、検証を自動化するのは困難です。形式仕様記述では数学的な表記ができるよう記法が定義されており、論理的な記述により事象を明確に定義することができます。

国際標準の動向

　海外と取引のある企業には、別の側面から形式手法の必要性が迫っています。形式手法が関係する国際標準の動向を整理してみましょう。

　ISO/IEC 61508は、2000年に刊行された電気・電子関連の国際安全規格です。日本で「機能安全」と呼ばれているこの規格は欧州主導で策定されたもので、安全度水準をSIL（Safety Integrity Level）で4段階に区分しています。ISO/IEC 61508においては、SIL2以上で形式手法を推奨しています。

　ISO/IEC 15408は、IT製品のセキュリティに関する国際標準です。情報セキュリティの実現度をEAL（Evaluation Assurance Level：評価保証レベル）で表しており、EAL5以上で「準形式的表現」、EAL7では「形式的表現」の利用が必須となっています。

　今後、戦略的に策定される規格による制限により、海外とのビジネスが制約される方向へ進むと専門家の間では考えられています。日本企業も形式手法に真剣に取り組むことが要求されると考えられます。

生産性に与える影響

　ここまでは品質という観点で形式手法を説明してきました。では、生産性についてはどうでしょうか。

　一般に品質・コスト・納期はトレードオフの関係にあり、品質を高めるにはより多くの工数が必要になると考えられます。形式手法で仕様を記述する場合、従来の（自然言語などによる）仕様記述よりも厳密に記述する分、工数は多く掛かります。

　しかし、ソフトウェア工学において上流工程の品質が悪ければ下流工程での手戻りが増え、全体の工数が大きくなることが知られています。形式手法を用いた場合、要求分析・設計の工数は多くなりますが、開発プロジェクト全体で見ると工数は少なくなると考えられます。

　日本フィッツ（現CSKシステムズ）の事例では、VDMを利用して上流工程での不具合をなくすことで、COCOMO IIの見積もりに対し約3倍もの生産性を達成したという報告があります。