한국   대만   중국   일본 
形式手法 - Wikipedia コンテンツにスキップ

形式手法

出典: フリ?百科事典『ウィキペディア（Wikipedia）』
Z言語 を使った 形式仕?記述 の例

形式手法 （けいしきしゅほう、 英 : 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] し、形式手法の利点を?調しすぎる姿勢を問題にする人?もいる。

主な形式手法とその記述法 [ 編集 ]

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

仕?記述言語

モデルチェッカ

脚注 [ 編集 ]

[ 脚注の使い方 ]
  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日時点におけるア?カイブ。 . https://web.archive.org/web/20061116210448/http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf 2006年11月16日 ??。 .  
  3. ^ Monin & Hinchey 2003 , pp. 3?4
  4. ^ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods" , IEEE Computer , 1996年4月
  5. ^ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" , Crosstalk: The Journal of Defense Software Engineering , 2003年1月
  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
  7. ^ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6 .
  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 Zurich 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年

?考文? [ 編集 ]

  • Monin, Jean Francois; 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」(再ライセンス) ?件に基づいて組み?まれている。

?連項目 [ 編集 ]

外部リンク [ 編集 ]

分野
コンセプト
指向
モデル
開?モデル
他のモデル
モデリング言語
主な人物
?連項目
ハ?ドウェア
コンピュ?タシステムの構造
ネットワ?ク
ソフトウェアの構造
ソフトウェア記法 （ 英語版 ）
と ツ?ル
ソフトウェア開?
計算理論
アルゴリズム
コンピュ?ティングの??
情報システム
セキュリティ
ヒュ?マンコンピュ?タ
インタラクション
?行性
人工知能
機械?習
グラフィックス
?用コンピュ?ティング
「 https://ja.wikipedia.org/w/index.php?title=形式手法&oldid=90759462 」から取得