形式手法
出典: フリー百科事典『ウィキペディア（Wikipedia）』
形式手法（Formal Methods）とは、計算機科学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である。そのアプローチは高度な信頼性（安全性やセキュリティなど）を求められるシステムでは特に重要であり、開発工程でエラーが入り込まないことを保証する。形式手法は要求仕様レベルや機能仕様レベルでは特に効果的であるが、実装レベル（例えばプログラム作成）でも完全な形式主義的開発は可能である。
目次 |
[編集] 分類
形式手法の利用はいくつかのレベルに分けられる:
- レベル0: 形式仕様記述を行い、プログラム自体は非形式主義的に行われる。「軽い形式手法」と呼ばれる。最も費用効果が高い選択と思われる。
- レベル1: 開発と検証が行われ、より形式主義的にプログラムを生成する。例えば、仕様記述からプログラム作成において詳細化と属性の証明が行われる。高信頼システムに適した選択である。
- レベル2: 自動定理証明によって完全に機械的に証明が行われる。非常に高価となり、間違いが混入することで生じる損失に見合わなければ実施されない（例えば、マイクロプロセッサ設計の重要な部分など）。
詳しくは後述する。
プログラム意味論の分類に対応して、形式手法は以下のように大別される:
- 表示的意味論では、システムの意味は領域理論で表現される。この場合、領域理論の性質によってシステムの意味が与えられるとする。しかし、あらゆるシステムが関数に直感的に表現できるわけではないとも言われている。
- 操作的意味論では、より単純な計算モデルの一連の動作によってシステムの意味が表現される。この場合、モデルの単純性が表現を明確にするとされる。しかし、これは意味論的な判断の先延ばしとも言われている（つまり、使用された単純な計算モデルの意味論の定義はどうなるのか？）。
- 公理的意味論では、システムがある処理を行う前と後の（真なる）状態によってシステムの意味を表現する。この場合、古典的論理学と関係が深い。しかし、単に実行前と実行後の状態を示しただけで実際にシステムが何をするかを表現したことになるのかとの疑念も言われている。
[編集] ライトウェイトな形式手法
実際の開発に携わる人々の中には、形式手法コミュニティが仕様記述と設計の完全な形式化を強調しすぎていると感じている[1][2]。彼らは対象となるシステム自体の複雑性だけでなく使用する言語の表現能力が完全か形式化を困難にしていると主張する。代替案として様々な軽量（ライトウェイト）な形式手法が提案されてきた。それらは部分的な仕様記述と応用に注力したものである。このようなライトウェイトな形式手法の例として、Alloy オブジェクトモデリング記法[3]、Z記法によるユースケース駆動型開発[4]、IFAD VDM ツールセット[5]がある。
[編集] 利用
形式手法は開発工程の様々な部分に適用可能である。ここではウォーターフォールモデルの用語を使用するが、他の開発手法でも形式手法は利用可能である。
[編集] 仕様記述
形式手法は開発対象システムの任意のレベルの仕様を記述するのに利用可能である。そのような形式的記述はその後の開発活動のガイドとなるだけでなく、開発されたシステムの機能が要求通りであるか正確性と完全性の観点での検証にも利用可能である。
従来から、形式仕様記述システムの必要性は注目されている。ALGOL 60の報告書の中でジョン・バッカスはプログラミング言語の文法の形式的記法（後にバッカス・ナウア記法、BNF記法と呼ばれるようになった）を提案した。バッカスはプログラミング言語の意味論の記法の必要性にも言及した。報告書にはBNF記法と同様の意味論に関する記法を将来提案すると書かれているが、それが現われることはなかった。
[編集] 開発
形式仕様記述ができると、それに従って実際の開発が行われる（すなわち、ソフトウェアやハードウェアに実体化させる）。例えば:
- 操作的意味論に基づく形式仕様記述の場合、実際のシステムの動作と仕様上の動作（それ自体が実行可能/シミュレート可能）を比較する。さらにツールによってはそのような仕様記述から自動的にコードを生成するものもある。
- 公理的意味論に基づく形式仕様記述の場合、仕様に記された事前状態と事後状態が実行コード内にアサーションとして組み込まれる。
[編集] 検証
形式仕様記述ができると、それを証明の根拠として使用することもある。
[編集] 人間による証明
場合によっては、システムの正当性の証明を行う動機は、システムの品質保証のためではなく、システムの動作をさらに理解したいためということがある。結果として正当性の証明を数学的証明の形式で行うこともある。自然言語を使い、あまり形式的でない形で証明が記述される。よい証明とは、他の人間が読んで理解できるものと言える。
このような手法への批判として、自然言語の曖昧さがエラーを見逃す原因となるとの指摘がある。微妙なエラーはそのような証明で見過ごされた低レベルな詳細部分に潜んでいることが多い。さらに、よい証明を作成するには高度な数学的専門知識が必要である。
[編集] 自動証明
一方、システムの正当性の証明を自動的に生成することに関心が集まりつつある。自動化技術は2つに分類される:
いずれの場合も人間の補助なしには機能しない。自動定理証明では、追跡すべき特性を人間が指定してやる必要がある。モデル検査ではうまく抽象化されたモデルを与えないと、膨大な数の状態によって身動きが取れなくなる。
これらシステムの提唱者は、詳細に渡ってアルゴリズム的に照合が行われるため、その結果は人間による証明よりも数学的にずっと正確であると主張する。これらシステムを使うための訓練は手で証明を書くための訓練よりも簡単であり、多くの人材を生み出せるとしている。
批判的な人々は、それらシステムの「神託」的正確を問題にする。それらは真実であると宣言しているが、その詳細は説明されない。また「検査機構の検査」と呼ばれる問題もある。検証に関わるプログラム自体が検証されていない場合、その結果を疑う余地があるだろう。
[編集] 批評
部分的な批評だけでなく、形式手法全体への批判もある。現状、人間の手による証明も自動的な証明も多大な時間（とお金）を要する。従って、形式手法はそのコストが十分利益に見合うか、エラーの混入が多大な損害に結びつく場合にのみ使われることになる。例えば、航空宇宙工学ではエラーの混入は死を意味するため、他の領域よりも形式手法が一般化している。
形式手法の提唱者は、それがソフトウェア危機の特効薬となると主張することもあった。もちろん多くの人々はソフトウェア危機に特効薬は存在しないと考えているし、形式手法の利点を強調しすぎる姿勢を問題にする人々もいる。
[編集] 主な形式手法とその記述法
以下に主な形式手法と形式手法の記述法を列挙する。
[編集] 関連項目
[編集] 参考文献
- ↑ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, 1996年4月
- ↑ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, 2003年1月
- ↑ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (2002年4月), pp. 256-290
- ↑ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
- ↑ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods", In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, 1998年10月
[編集] 外部リンク
この記述は GNU Free Documentation License のもとに公開されているコンピュータ用語辞典『 Free On-line Dictionary of Computing (FOLDOC) 』に基づいています。
