「形式手法」の版間の差分

削除された内容追加された内容

インライン

2021年4月28日 (水) 23:22時点における版

形式手法（けいしきしゅほう、英: formal methods）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である^[1]。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている^[2]。

形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う^[3]。

分類

形式手法はいくつかの水準で使用可能である:

水準0: 形式仕様記述を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得ることができる選択である。
水準1: 形式手法を使って開発と検証を行い、より形式主義的にプログラムを生成する。例えば、仕様記述からのプログラム作成において詳細化と属性の証明を行う。高信頼システムに適した選択である。
水準2: 自動定理証明によって完全に機械的な証明を行う。道具を整備するのに費用がかかるか、厳密である必要がありシステムを記述するのに手間がかかる。間違いが混入することで生じる損失に見合わなければ実施しない（例えば、マイクロプロセッサ設計の重要な部分など）。

詳しくは後述する。

プログラム意味論の分類に対応して、形式手法は以下のように大別する:

表示的意味論: 表示的意味論では、システムの意味は領域理論で表現する。この場合、領域理論の性質によってシステムの意味を与える。しかし、あらゆるシステムが関数に直感的に表現できるわけではないとも言われている。
操作的意味論: 操作的意味論では、より単純な計算モデルの一連の動作によってシステムの意味を表現する。この場合、モデルの単純性が表現を明確にする。しかし、これは意味論的な判断の先延ばしとも言われている（つまり、使用された単純な計算モデルの意味論の定義はどうなるのか？）。
公理的意味論: 公理的意味論では、システムがある処理を行う前と後の（真なる）状態によってシステムの意味を表現する。この場合、古典的論理学と関係が深い。しかし、単に実行前と実行後の状態を示しただけで実際にシステムが何をするかを表現したことになるのかとの疑念も言われている。

軽量(light weight)形式手法

実際の開発に携わる人々の中には、形式手法コミュニティが仕様記述と設計の完全な形式化を強調しすぎていると感じている^[4]^[5]。彼らは対象となるシステム自体の複雑性だけでなく使用する言語の表現能力が完全かどうかが形式化を困難にしていると主張する。代替案として様々な軽量（ライトウェイト）な形式手法が提案されてきた。それらは部分的な仕様記述と応用に注力したものである。このようなライトウェイトな形式手法の例として、型システム、uppaal Alloy オブジェクトモデリング記法^[6]、Z言語によるユースケース駆動型開発^[7]、CSK VDM ツールセット^[8]がある。

利用

形式手法は開発工程の様々な部分に適用可能である。

仕様記述

形式手法は開発対象システムの任意のレベルの仕様を記述するのに利用可能である。そのような形式的記述はその後の開発活動のガイドとなるだけでなく、開発されたシステムの機能が要求通りであるか正確性と完全性の観点での検証にも利用可能である。

従来から、形式仕様記述システムの必要性は注目されている。ALGOL 58の報告書^[9]の中でジョン・バッカスはプログラミング言語の文法の形式的記法（後にバッカス・ナウア記法、BNF記法と呼ばれるようになった^[10]）を提案した。バッカスはプログラミング言語の意味論の記法の必要性にも言及した。報告書にはBNF記法と同様の意味論に関する記法を将来提案すると書かれているが、それが現われることはなかった。

開発

形式仕様記述ができると、それに従って設計を行い、実際の開発を行う（すなわち、ソフトウェアやハードウェアに実体化させる）。例えば:

操作的意味論に基づく形式仕様記述の場合、実際のシステムの動作と仕様上の動作（それ自体が実行可能/シミュレート可能）を比較する。さらにツールによってはそのような仕様記述から自動的にコードを生成するものもある。
公理的意味論に基づく形式仕様記述の場合、仕様に記された事前状態と事後状態が実行コード内にアサーションとして組み込まれる。

検証

形式仕様記述ができると、それを証明の根拠として使用することもある。

人間による証明

場合によっては、システムの正当性の証明を行う動機は、システムの品質保証のためではなく、システムの動作をさらに理解したいためということがある。結果として正当性の証明を数学的証明の形式で行うこともある。自然言語を使い、あまり形式的でない形で証明が記述される。よい証明とは、他の人間が読んで理解できるものと言える。

このような手法への批判として、自然言語の曖昧さがエラーを見逃す原因となるとの指摘がある。微妙なエラーはそのような証明で見過ごされた低レベルな詳細部分に潜んでいることが多い。さらに、よい証明を作成するには高度な数学的専門知識が必要である。

自動証明

一方、システムの正当性の証明を自動的に生成することに関心が集まりつつある。自動化技術は2つに分類される:

自動定理証明では、何もないところから形式的証明を生成する。入力となるのはシステムの説明、論理的公理群、推論規則群である。
モデル検査では、実行時に取りうる全状態を検索し、一定の特性を照合する。

一部の自動定理証明は人間の補助なしには機能せず、追跡すべき特性を人間が指定してやる必要がある。モデル検査ではうまく抽象化されたモデルを与えないと、膨大な数の状態によって身動きが取れなくなる。

これらシステムの提唱者は、詳細に渡ってアルゴリズム的に照合が行われるため、その結果は人間による証明よりも数学的にずっと正確であると主張する。これらシステムを使うための訓練は手で証明を書くための訓練よりも簡単であり、多くの人材を生み出せるとしている。

批判的な人々は、それらシステムの「神託」的性格を問題にする。それらは真実であると宣言しているが、その詳細は説明されない。また「検査機構の検査」と呼ばれる問題もある。検証に関わるプログラム自体が検証されていない場合、その結果を疑う余地があるだろう。

批評

部分的な批評だけでなく、形式手法全体への批判もある。現状、人間の手による証明も自動的な証明も多大な時間（とお金）を要する。従って、形式手法はそのコストが十分利益に見合うか、エラーの混入が多大な損害に結びつく場合にのみ使われることになる。例えば、航空宇宙工学ではエラーの混入は死を意味するため、他の領域よりも形式手法が一般化している。

形式手法の推進者の中には、それがソフトウェア危機の特効薬となると主張する者もあった。もちろん多くの人々はソフトウェア危機に特効薬は存在しないと考えている^[11]し、形式手法の利点を強調しすぎる姿勢を問題にする人々もいる。

主な形式手法とその記述法

以下に主な形式手法と形式手法の記述法を列挙する。

仕様記述言語

アクターモデル
プロセス計算
- CSP
- LOTOS
- π計算（英語版）
ペトリネット
抽象状態機械（英語版） (ASM)
Alloy
ANSI/ISO C Specification Language（英語版） (ACSL)
B-Method
CADP
Common Algebraic Specification Language (CASL)
Esterel
Lustre
mCRL2
Perfect Developer
RAISE
Rebeca Modeling Language
SPARK Ada（英語版）
Specification and Description Language (SDL)
Temporal logic of actions (TLA)
uppaal
USL
VDM
- VDM-SL
- VDM++
Z言語

モデルチェッカ

脚注

[脚注の使い方]

^ R. W. Butler (2001年8月6日). “What is Formal Methods?”. 2006年11月16日閲覧。
^ C. Michael Holloway. Why Engineers Should Consider Formal Methods. 16th Digital Avionics Systems Conference (27–30 October 1997). オリジナルの2006年11月16日時点におけるアーカイブ。 2006年11月16日閲覧。.
^ Monin & Hinchey 2003, pp. 3–4
^ 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月
^ Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.
^ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.
^ フレデリック・ブルックス、『銀の弾などない』 (No Silver Bullet) 、1986年

参考文献

Monin, Jean François; Hinchey, Michael G. (2003), Understanding formal methods, Springer, ISBN 1-85233-247-6
Jonathan P. Bowen and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering,Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, Association for Computing Machinery, 2004.
Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, Taylor & Francis, 2010, pages 308–320.

この記事は2008年11月1日以前にFree On-line Dictionary of Computingから取得した項目の資料を元に、GFDL バージョン1.3以降の「RELICENSING」(再ライセンス) 条件に基づいて組み込まれている。

外部リンク

Formal Methods Wiki
Formal Methods Europe (FME)
Formal method keyword on Microsoft Academic Search
Foldoc:formal methods
Evidence on Formal Methods uses and impact on Industry Supported by the DEPLOY project (EU FP7)

[butler-1] R. W. Butler (2001年8月6日). “What is Formal Methods?”. 2006年11月16日閲覧。

[2] C. Michael Holloway. Why Engineers Should Consider Formal Methods. 16th Digital Avionics Systems Conference (27–30 October 1997). オリジナルの2006年11月16日時点におけるアーカイブ。 2006年11月16日閲覧。.

[3] Monin & Hinchey 2003, pp. 3–4

[JacksonWing1996-4] Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, 1996年4月

[GeorgeVaughn2003-5] Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, 2003年1月

[Jackson2002-6] 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

[Denny2005-7] Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.

[AgerholmLarsen1998-8] 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月

[9] Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.

[10] Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.

[11] フレデリック・ブルックス、『銀の弾などない』 (No Silver Bullet) 、1986年

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

@@ 35行目: / 35行目: @@
 === 検証 ===
-形式仕様記述ができると、それを[[証明]]の根拠として使用することもある。
+形式仕様記述ができると、それを[[証明 (数学)|証明]]の根拠として使用することもある。
 ====人間による証明====
-場合によっては、システムの正当性の証明を行う動機は、システムの品質保証のためではなく、システムの動作をさらに理解したいためということがある。結果として正当性の証明を数学的[[証明]]の形式で行うこともある。[[自然言語]]を使い、あまり形式的でない形で証明が記述される。よい証明とは、他の人間が読んで理解できるものと言える。
+場合によっては、システムの正当性の証明を行う動機は、システムの品質保証のためではなく、システムの動作をさらに理解したいためということがある。結果として正当性の証明を数学的[[証明 (数学)|証明]]の形式で行うこともある。[[自然言語]]を使い、あまり形式的でない形で証明が記述される。よい証明とは、他の人間が読んで理解できるものと言える。
 このような手法への批判として、自然言語の[[曖昧]]さがエラーを見逃す原因となるとの指摘がある。微妙なエラーはそのような証明で見過ごされた低レベルな詳細部分に潜んでいることが多い。さらに、よい証明を作成するには高度な数学的専門知識が必要である。