形式けいしき手法しゅほう

形式けいしき手法しゅほう（けいしきしゅほう、英えい: 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]

表ひょう話はなし編へん歴れきコンピュータ科学かがく
ハードウェア	プリント基板きばん周辺しゅうへん機器きき Integrated Circuit (IC) Very Large Scale Integration (超大ちょうだい規模きぼ集積しゅうせき回路かいろ、VLSI) Systems on Chip (SoC) エネルギー消費しょうひ (グリーン・コンピューティング) EDA ハードウェアアクセラレーション
コンピュータシステムの構造こうぞう	コンピュータ・アーキテクチャ組くみ込こみシステムリアルタイムシステムディペンダビリティ
ネットワーク	ネットワーク・アーキテクチャ（英語えいご版ばん）通信つうしんプロトコルネットワーク・コンポーネント（英語えいご版ばん）ネットワーク・スケジューラ（英語えいご版ばん）ネットワーク性能せいのう評価ひょうか（英語えいご版ばん）ネットワーク・サービス（英語えいご版ばん）
ソフトウェアの構造こうぞう	インタプリタミドルウェア仮想かそうマシンオペレーティングシステムソフトウェア品質ひんしつ
ソフトウェア記法きほう（英語えいご版ばん）とツール	プログラミングパラダイムプログラミング言語げんごコンパイラドメイン固有こゆう言語げんごモデリング言語げんごソフトウェアフレームワーク統合とうごう開発かいはつ環境かんきょうソフトウェア構成こうせい管理かんりソフトウェアライブラリソフトウェアリポジトリ
ソフトウェア開発かいはつ	ソフトウェア開発かいはつプロセス要求ようきゅう分析ぶんせきソフトウェア設計せっけいソフトウェア構築こうちく（英語えいご版ばん）ソフトウェアデプロイメントソフトウェアメンテナンスプログラミングチーム（英語えいご版ばん）オープンソースモデル
計算けいさん理論りろん	計算けいさんモデル形式けいしき言語げんごオートマトン理論りろん計算けいさん可能かのう性せい理論りろん計算けいさん複雑ふくざつ性せい理論りろんコンピュータ科学かがくにおける論理ろんり学がく（英語えいご版ばん）意味いみ論ろん
アルゴリズム	アルゴリズム（英語えいご版ばん）アルゴリズム解析かいせきアルゴリズム効率こうりつ（英語えいご版ばん）乱みだれ択よアルゴリズム計算けいさん幾何きか学がく
コンピューティングの数学すうがく	離散りさん数学すうがく確かく率りつ統計とうけい学がく数学すうがくソフトウェア情報じょうほう理論りろん解析かいせき学がく数値すうち解析かいせき
情報じょうほうシステム	データベース管理かんりシステム情報じょうほうストレージシステム企業きぎょう情報じょうほうシステム社会しゃかい情報じょうほうシステム（英語えいご版ばん）地理ちり情報じょうほうシステム意思いし決定けってい支援しえんシステムプロセス制御せいぎょシステムマルチメディア情報じょうほうシステム（英語えいご版ばん）データマイニング電子でんし図書館としょかんコンピューティング・プラットフォームデジタルマーケティング World Wide Web 情報じょうほう検索けんさく
セキュリティ	暗号あんごう理論りろん形式けいしき手法しゅほうセキュリティ・サービス（英語えいご版ばん）侵入しんにゅう検知けんちシステムハードウェア・セキュリティ（英語えいご版ばん）ネットワーク・セキュリティ情報じょうほうセキュリティアプリケーション・セキュリティ（英語えいご版ばん）
ヒューマンコンピュータインタラクション	インタラクションデザインソーシャル・コンピューティング（英語えいご版ばん）ユビキタスコンピューティング可視かし化かアクセシビリティ
並行へいこう性せい	並行へいこうコンピューティング並列へいれつコンピューティング分散ぶんさんコンピューティングマルチスレッディングマルチプロセッシング
人工じんこう知能ちのう	自然しぜん言語げんご処理しょり知識ちしき表現ひょうげんと推論すいろんコンピュータビジョン自動じどう計画けいかくとスケジューリング検索けんさく手法しゅほう制御せいぎょ手法しゅほう人工じんこう知能ちのうの哲学てつがく（英語えいご版ばん）分散ぶんさん人工じんこう知能ちのう（英語えいご版ばん）
機械きかい学習がくしゅう	教師きょうしあり学習がくしゅう教師きょうしなし学習がくしゅう強化きょうか学習がくしゅうマルチタスク学習がくしゅう（英語えいご版ばん）交差こうさ検証けんしょう
グラフィックス	アニメーションレンダリング画像がぞう編集へんしゅう GPU 複ふく合あい現実げんじつバーチャル・リアリティ画像がぞう圧縮あっしゅくソリッドモデリング
応用おうようコンピューティング	電子でんし商取引しょうとりひき企業きぎょうアプリケーション計算けいさん数学すうがく（英語えいご版ばん）計算けいさん物理ぶつり学がく計算けいさん化学かがく計算けいさん生物せいぶつ学がく計算けいさん社会しゃかい科学かがく計算けいさん工学こうがく（英語えいご版ばん）健康けんこう情報じょうほう学がくデジタルアート電子でんし出版しゅっぱんサイバー戦争せんそう電子でんし投票とうひょうコンピュータゲームワードプロセッサーオペレーションズ・リサーチ教育きょういく工学こうがく文書ぶんしょ管理かんりシステム
概要がいよう（英語えいご版ばん）カテゴリブックコモンズ