フォーマルメソッド（形式手法）をご存じだろうか。これは，ほとんどの場合日本語で記述される「要求仕様」を，プログラミング言語によるコーディングと同じように，厳密に「仕様記述言語」で定義する手法のことである。

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

　言うまでもないが，システム全体の品質を高めるためには，要求定義などの上流工程の欠陥をどれだけ減らすかが大きなカギとなる。そういう意味で，「フォーマルメソッド」は高品質なシステムを作るための重要な武器になり得ると，記者は思っている。

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

　しかし，組み込み開発の現場では，この状況が変化している。フォーマルメソッドの一つ「VDM（Vienna Development Method）」を利用するコンサルティング・サービスや開発・設計支援サービス（サービスの総称はFolha＝FOrmal approach Leads Highly reliable Applications）を，製造業（メーカー）の組み込み開発向けに展開しているCSKシステムズの佐原 伸氏（製造グループ VDM推進課 理事）は次のように語る。

　「2005年～2006年ころは，『フォーマルメソッド？なんじゃそりゃ』という感じで拒絶する人が多かったが，2007年春くらいから，興味を持つメーカーが急増している。明らかに流れが変わった。『フォーマルメソッドなんて関係ない』という人はまずいなくなった」。

経済産業省のガイドラインも追い風に

　CSKシステムズは，フォーマルメソッドに力を入れている大手SIerである。同社は2005年に，VDM用の支援ツール「VDMTools」の権利をデンマークの開発元から買い取って無償で提供しているほか，2007年4月には，製造業の顧客向け事業グループである「製造グループ」内に「VDM推進課」と呼ぶVDMの専門組織を設置（スタッフ数は11人）。VDM推進課が，VDMを利用したコンサルティングサービスやVDMの啓蒙／研修のコア部隊となっている。

　VDMを利用できるエンジニアの育成にも力を入れており，VDMの研修カリキュラム（VDMの仕様記述言語である「VDM++」の言語仕様とVDM++によるモデリングを学ぶ5日間の研修）を履修済みの組み込み開発エンジニアは約200人に上る（CSKシステムズ，CSKシステムズ西日本，CSKシステムズ中部を合わせた数）。これは，組み込み開発エンジニア全体の2～3割に当たるという。ちなみに佐原氏によれば，仕様記述言語であるVDM++の言語仕様そのものは「プログラミングができる人であればJavaよりも易しい」という。

　佐原氏によれば，2007年春くらいからフォーマルメソッドに対する拒否反応が減ってきた原因は主に2つある。1つは，多くのメーカーがプロセス改革の次のターゲットとして，本気で「要求定義フェーズの改革」を考え出したこと。組み込み開発で不具合をなくすために，各メーカーとも設計～テスト工程のプロセス改革は進めている。しかし，要求定義フェーズの改革は，これまで手つかずだった。ここにメスを入れたい，と考えるメーカーが増えているのだ。「最近は，要求定義のプロセス改革の具体的な手段としてフォーマルメソッドに興味を持つメーカーが多い。こうしたメーカーは，フォーマルメソッドで『検証できる要求仕様』を作成し設計工程に送れるようにすることを検討している」（佐原氏）。

　もう1つは，「フォーマルメソッド」や「形式手法」という言葉を知っている人が以前よりも増えたこと。これは，2006年6月に公表された経済産業省の「情報システムの信頼性向上に関するガイドライン」や産業機器などに向けた国際安全規格「ISO／IEC 61508」でフォーマルメソッド（形式手法）が盛り込まれたことが大きい。参考までに，経済産業省のガイドラインでは，「IV.技術に関する事項」の章に，次のように記述している。

（２）形式手法・ツール等の活用
情報システム供給者は、自然言語による要求仕様作成作業の誤りを極力排除し、ソフトウェア設計の一層の精度向上を図るため、形式手法（仕様記述言語による仕様記述とモデル検証）及びツール等の適用可能性及び効果等を評価の上、積極的に活用を検討することが望ましい。
＜実施例＞
設計段階において、特に高い水準の信頼性・安全性が求められる部分に対して形式手法を適用する。

　フォーマルメソッドへの拒否反応が減り，興味を持つメーカーが増えてきたために，CSKシステムズのVDMを利用したコンサルティングサービスを受けるメーカーも増えているという。現在のところ，コンサルティングを受けているメーカーは10社弱。いずれも，まだ実開発ではなく，プロトタイプ的に導入したり要求仕様のプロセス改革を検討したりしている段階だが「実開発まで行く可能性は高い」（製造グループ理事の小川 千之氏）という。

　ここまで読んで，「結局，組み込み開発にしか使えないのか」と思ったエンジニアも多いと思う。しかし，「企業情報システム開発への適用にもまったく問題はない」と佐原氏は語る。実際，CSKシステムズでは，証券会社用パッケージのサブシステムの開発にVDM++を適用したことがある（サブシステムの規模は約8万行）。

　「高品質が求められるミッション・クリティカルな企業情報システム開発は，本来，フォーマルメソッドで品質を担保すべき。要求仕様を仕様記述言語で厳密に記述することで，企業にとっての『資産』として要求仕様を残せるメリットもある」と佐原氏は言う。CSKシステムズでは2008年4月から，VDMを利用するコンサルティング・サービスや開発・設計支援サービスの対象を，組み込み開発から企業情報システム開発へと広げる予定である。