形式手法
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/06/24 14:45 UTC 版)
形式手法（けいしきしゅほう、英: formal methods）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である[1]。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている[2]。
- ^ 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年
形式手法
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/11/21 08:28 UTC 版)
合成したいプログラムの性質を論理式で表し、それを自動的に証明する過程でプログラムが合成される。
※この「形式手法」の解説は、「プログラム合成」の解説の一部です。
「形式手法」を含む「プログラム合成」の記事については、「プログラム合成」の概要を参照ください。
形式手法
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/16 06:41 UTC 版)
「ソフトウェア開発工程」の記事における「形式手法」の解説
形式手法は要求/仕様記述/設計段階でのソフトウェア（およびハードウェア）問題への数学的対処法である。形式手法の例として、Bメソッド・ペトリネット・RAISE・VDMなどがある。形式仕様記述もZ記法など様々な手法がある。より一般化すれば、有限状態機械のシステムを設計することでオートマトン理論を応用してアプリケーションの動作を解明する。 有限状態機械（FSM）に基づいた方法論で実行可能ソフトウェアの仕様記述ができ、従来的なコーディング工程を省くことができる（仮想有限状態機械及びイベント駆動有限状態機械）。 形式手法はアビオニクスソフトウェアなどの安全性が重要とされるソフトウェアでよく採用されている。DO178Bなどのソフトウェアの安全性保証標準規格では、形式手法の採用が義務付けられている（レベルAの場合）。 形式手法は開発工程に様々な形で入り込んできつつある。
※この「形式手法」の解説は、「ソフトウェア開発工程」の解説の一部です。
「形式手法」を含む「ソフトウェア開発工程」の記事については、「ソフトウェア開発工程」の概要を参照ください。
形式手法
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/20 16:21 UTC 版)
形式手法は、ソフトウェアやハードウェアの解析に用いられる用語であり、厳密に数学的な手法によって解析結果を得ることを意味する。数学的手法としては、表示的意味論、公理的意味論、操作的意味論、抽象解釈などがある。 実行時エラーを全て検出することは不可能であることが証明されており、任意のプログラムが正しく動作するかエラーになるかを判定する機械的手法はない。これは1930年代のアラン・チューリングやライスの研究で判明した（チューリングマシンの停止問題およびライスの定理）。決定不能な問題ではあるが、近似的な解でも有効である。 形式的な静的コード解析の実装方法には以下のようなものがある: モデル検査は、有限の状態を持つシステムを対象とし、無限に状態を持つシステムを抽象化によって状態数を有限個に減らして行うこともある。 データフロー解析は、プログラムの各点で変数群の取りうる値についての情報を集める技法である。 抽象解釈は、プログラムの個々の文が抽象機械の状態に何らかの影響を与える様子をモデル化したものである（つまり、ソフトウェアを個々の文の数学的属性と宣言に基づいて「実行」する）。抽象機械は解析しやすいようになるべく単純化されるので、実際のプログラムを完全に表すわけではない（もとのシステムで真である属性が抽象システムで常に真とは限らない）。うまくいけば、抽象解釈は「健全」とされる（抽象システムで真である全属性はもとのシステムでも真だといえる）。例えば、Frama-cやPolyspaceといったツールは、抽象解釈の技法を使っている。 表明をプログラム内で使うことは、ホーア論理で最初に示唆された。一部のプログラミング言語は表明をツールとしてサポートしている（例えば、AdaのサブセットであるSPARK、ESC/JavaやESC/Java2を使った Java Modeling Language (JML)、C言語を ACSL (ANSI/ISO C Specification Language) で拡張する Frama-c WP（weakest precondition、最弱事前条件）プラグインがある）。
※この「形式手法」の解説は、「静的コード解析」の解説の一部です。
「形式手法」を含む「静的コード解析」の記事については、「静的コード解析」の概要を参照ください。
固有名詞の分類
- 形式手法のページへのリンク
