形式手法におけるツールの充実や，ソフトウェアの品質に対する要求の高まりを受けて，形式手法は改めて注目されてきています．ただし，形式手法・ツールにはその目的に応じて多種多様な種類があり，また個々の手法・ツールを効果的に用いるためには注意深く適用方法を検討する必要があります．
このサイトでは，形式手法の利用を促進することを目指し，目的の異なる様々な手法・ツールや実際の適用ノウハウに関する情報を集め，公開しています．
本サイトと運営者についてのより詳細な情報はこちらをご参照ください．
お知らせ・更新履歴
- 2010/04/13
- 「付録： 形式手法7つの「神話」（後）」ページを追加しました．
- 2010/03/28
- 「付録： 形式手法7つの「神話」（前）」ページを追加しました．
- 2010/03/23
- 「リンク集（総合・基本） 」ページ，「リンク集（適用事例・ノウハウ） 」ページを更新しました．
- 2010/03/22
- 「リンク集（モデル検査ツール） 」，「リンク集（形式仕様記述ツール） 」ページを更新しました．
- 2010/03/15
- 「適用事例 」ページを更新しました．
形式手法7つの「神話」（後）
このページでは，下記文献における7つの神話（根拠なく主張されていること）に関する議論引用のの続きです．前編はこちら．
Seven Myths of Formal Methods
Anthony Hall, IEEE Software, vol. 7, no. 5, pp. 11-19, 1990
形式手法7つの「神話」（前）
このページでは，下記文献における7つの神話（根拠なく主張されていること）に関する議論を引用します．「＊＊だから完璧」とか「＊＊だから論外」とか表面的なところで思考を止めず，「自分の問題（プロジェクト）に対してどう使うのか，それにより何ができて何ができないのか」に関する検討が必要，という当然の結論について，適用経験に基づいて議論しています．
Seven Myths of Formal Methods
Anthony Hall, IEEE Software, vol. 7, no. 5, pp. 11-19, 1990
書籍・リンク集（適用事例・ノウハウ）
このページでは，形式手法の適用事例や適用ノウハウ・ガイドラインについての書籍，論文，Webサイトに関する情報をまとめていきます．
ツールリンク集（総合・基本）
このページでは総合的な開発ツールや，他ツールと組み合わせて利用できる基本ツールを配布，販売等しているWebサイトの情報をまとめています．分類は一元的ではないため，ツールリンク集（モデル検査），ツールリンク集（形式仕様記述）もご参照下さい．なお，コメントは運営者の一意見ですので，それを踏まえた上で参考にして下さい．
イベント案内
このページでは運営者が「個人的に」関わっているイベント等の情報を載せています．偏った情報になりますが，ご参考にしていただければと思います．
ツールリンク集（形式仕様記述）
このページでは形式仕様記述ツールを配布，販売等しているWebサイトの情報をまとめています．分類は一元的ではないため，ツールリンク集（モデル検査），ツールリンク集（総合・基礎）も併せてご参照下さい．なお，コメントは運営者の一意見ですので，それを踏まえた上で参考にして下さい．
ツールリンク集（モデル検査）
このページではモデル検査ツールを配布，販売等しているWebサイトの情報をまとめています．分類は一元的ではないため，ツールリンク集（形式仕様記述），ツールリンク集（総合・基礎）も併せてご参照下さい．なお，コメントは運営者の一意見ですので，それを踏まえた上で参考にして下さい．
適用事例 - 航空業界
Airbus、Boeing、Astium、Hispano-Suizaの事例が著名。
DO-178Cなどのソフトウェア認証基準に対応するため形式手法の適用が進む。
EUのFramework Programme(FP6, FP7)のファンドで開発したツールを使うケースも多い。
航空機のシステムを開発する際に、モデルベースの設計からモデル検査ツール、定理証明ツールに落とし込む手法が確立しつつある。
パフォーマンス解析、信頼性解析においても形式手法を用いている。
また、ソフトウェアを安全に配布する仕組みについても、セキュアな方式を形式手法を用いて実現する仕組みの検討が進められている。
（随時更新予定）
