フォーマルメソッドの可能性、限界はどこなんだろう

少し前に関わりかけていた案件で、人命に関わることなのでフォーマルメソッド(wikipedia:形式手法)を使った方がいいかなと思ったことがあって、意識の片隅にはあったんですが、「「拒否反応」がなくなり実用段階に入った「フォーマルメソッド」：ITPro」という記事を見て、時代は変化してきたのかな。オブジェクト指向分析設計手法を模索していたころに、システム設計をさらに改善する手法としてフォーマルメソッドに興味を持った時期が有って、「An Introduction to Formal Specifications and Z」なんかを読んだんでしたっけ。
フォーマルメソッドのメリットは、

要求仕様を仕様記述言語で厳密に定義（モデリング）することで，要求仕様のあいまいさがなくなるほか，ライブラリを作成しておけば「要求仕様の再利用」も可能になる。構文チェックや型チェック，インタプリタによる動的テストにより，要求仕様の正しさもツールで検証できる。結果的に，要求定義フェーズの欠陥を大幅に減らせる。

ですが、同時に

ただし，「仕様記述言語を学ぶのが難しい」という理由で，これまでフォーマルメソッドへの拒否反応は非常に大きかった。わざわざ仕様記述言語で要求仕様を記述するよりも，これまで通り日本語で書いた方がはるかに楽だからだ。

というデメリットが有って、実際の適用は限定的でした。学ぶのが難しいというより、あいまいさが含まれていることの多い要求から形式的に仕様を記述するのは大変といった方がいいかな。制御システム、特に原子炉の制御とか医療機器などの場合は、取り返しの付かない人身事故につながりかねませんから、要求が比較的明確で有ることと相まって形式化のコストに見合うメリットがあるでしょう。でも、ビジネス分野では要求のあいまさとか、プロジェクト途中での要求の変化とかが問題にあります。プロジェクトにかけられるコストは当然限られいますから、形式化のコストにメリットが釣り合わないという思いが強くなって、その時点ではそれ以上進めること無いままでした。
ここでなぜフォーマルメソッドに再度関心を持ち出したかというと、「Googleを支える技術 ?巨大システムの内側の世界 (WEB+DB PRESSプラスシリーズ)」を読んだときにも思ったのですが、システムアーキテクチャの並列化が進む中で、いままで非実用的と思われていた物が日の目を見るようになるのではないかと最近思っているからです。もちろん鋭いひとは私なんかよりずっと先にそんな問題意識を持っているようで、最近関数型言語に関心が集まっているのはその現れかと。この辺り、自分の中でも纏めたいなとは思っているんですが、基本的なことろを今更ですが学び直さないといけないと自分の不勉強さを反省しきり。
この記事ではVDM(wikipedia:VDM)が取り上げられていましたが、いろいろ提案されていた手法の中でもVDMが主流になるのかな。VDMとみてIBMのウィーン研究所を思い出していまいましたが、ここはソフトウェア開発にいろいろ影響与える成果をだしているような。