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

[阿部 功二 CSKシステムズ，MONOist]

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

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

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

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

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

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

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

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

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

※コラム：UMLと形式手法

ご存じのとおり、UMLは親しみやすい表記で、設計者の考えを説明するのに適しています。ダイヤグラムを多用することで、モデルを視覚的にとらえることができる点がUMLのメリットですが、厳密な定義ができるわけではありません。

UMLもOCLを利用して制約を記述できるように拡張されており、形式手法に近づいてきました。しかし、もともと分かりやすさを追求してきたUMLと、厳密さ・正しさを追求してきた形式手法を統合するのは難しく、現時点では別々に考える方が実用的です。UMLと形式仕様記述は同じことを表現するためのものではないので、どちらが良いということではなく、補完関係にあるといえるでしょう。

例えば、システムをマクロでとらえて抽象レベルの高いモデルを検討する部分はUMLで行います。そして、詳細化と厳密な定義は形式仕様記述で行います。複雑な並行処理におけるデッドロックの検出には形式検証を利用するなど、UMLと形式手法を組み合わせるのが効果的です。

国際標準の動向

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

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

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

EAL	名称	評価概要
EAL7	Formally verified designed and tested	サブシステムレベルまでの設計が形式的表現、開発者による分析・テストの全てを評価者が再確認
EAL6	Semiformally verified designed and tested	モジュールレベルまでの設計が準形式的表現、非常に高度の攻撃に対抗
EAL5	Semiformally designed and tested	実装表現レベルのセキュリティ機能を全て確認、サブシステムレベルまでの設計が準形式的表現、隠れチャネル分析、高度の攻撃に対抗
EAL4	Methodically designed, tested, and reviewed	モジュールレベルまで確認、実装表現レベル（最も具体的レベルの設計：例えばソースコードレベル）の部分的確認、普通程度の攻撃に対抗
EAL3	Methodically tested and check	サブシステムレベルまでの開発者テスト結果の確認、構成管理システム使用の確認、開発者環境の確認、開発者による誤使用分析
EAL2	Structurally tested	サブシステムレベルまでセキュリティ機能設計の確認、構成管理の確認、開発者による機能強度、脆弱性分析、評価者による侵入テスト
EAL1	Functionally Tested	セキュリティ機能仕様、マニュアルの確認、評価者によるテスト

表1　ISO/IEC 15408のEAL（出典：IPA「ISO/IEC 15408のセキュリティ評価・認証」）

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

生産性に与える影響

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

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

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

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