「形式手法」を、システムの開発に活用するベンダーやユーザー企業が増えている。仕様の記述で漏れをなくす、従来型のテストでは発見しにくいバグを見つける、などが狙いだ。経済産業省が6月に公開した信頼性ガイドラインにも、推奨手法として掲載された。古くからある形式手法が注目され始めたのは、普及を阻んでいた“扱いにくさ”をカバーするツールが登場し、活用のノウハウが蓄積されたからである。
本記事は日経コンピュータ7月24日号からの抜粋です。そのため図や表が一部割愛されていることをあらかじめご了承ください。本「特集2」の全文をお読みいただける【無料】サンプル版を差し上げます。お申込みはこちらでお受けしています。なお本号のご購入はバックナンバーをご利用ください。
「キャッシュ・メモリーの制御に関する処理で、いくらテストしても原因が特定できなかったバグを形式手法で取り除くことができた」。富士通研究所 ITコア研究所ソフトウェアイノベーション研究部の原裕貴部長は、昨年9月に米国拠点で上げた“成果”をこう話す。CSKシステムズは、証券業務のパッケージ・ソフト「TradeOne」の開発で形式手法を採用。「仕様記述の段階で、漏れや矛盾といった欠陥を排除できたため、事実上のバグ・ゼロを実現した」（通信グループVDM担当の佐原伸理事）――。
さまざまなシステムの基盤となるミドルウエアや、ミッション・クリティカルなシステムの開発において、多くのベンダーやユーザー企業が形式手法が採用し始めた。形式手法を用いて厳密に仕様を記述することで、仕様のあいまいさを排除したり、矛盾を見つけたりできるからだ。
CSKシステムズは「業務処理システムに形式手法を使えるという確信が得られた」（佐原理事）として、今後、ユーザー企業から請け負ったシステム開発にも形式手法を用いる計画である。「2006年中に、2～3件は始めたい」（同）という。
普及を阻害する要因が減った
形式手法とは、ある規則にのっとって仕様を厳密に記述するもの。ここでの“厳密”とは、解釈が一通りしかできないことと、論理的な矛盾がないことを意味する。そのための専用言語が形式仕様記述言語であり、記述した仕様を形式仕様と呼ぶ。
 |
| 図1●形式手法のメリットと課題 |
さらに、システム開発における概要設計と詳細設計のように、機能（外部仕様）とそれを実現するための仕様（内部仕様）の両方を形式仕様記述言語で記述し、その間で矛盾が存在しないかどうかを検証することも、形式手法である（図1）。外部仕様で記述したことを内部仕様が網羅しているかも、チェックできる。最近、ベンダーが注目しているのは、厳密な記述よりも、こちらの検証のほうだ。
今、形式手法に光が当たっているのは、ニーズとシーズの両面で変化があったから。前者では、相次ぐシステム障害などを受けて経済産業省が、「情報システムの信頼性向上に関するガイドライン」の中で、高い信頼度が必要なシステムへの形式手法の適用を推奨した。日本版SOX法（企業改革法）に代表される内部統制の実現でも期待がかかる。NTTデータ 技術開発本部の山本修一郎副本部長は、「内部統制では、システムが規定の業務フローやセキュリティ・ポリシーを守っていることを証明することが求められる。形式手法はその手段となる」と語る。
一方のシーズ面では、これまで形式手法の普及を阻害してきた“使い勝手の悪さ”が改善されてきた。「厳密な記述が難しい」、「記述が二度手間になる」に対しては、各社が、既存の言語を使えるようなツールを開発。「検証範囲が広すぎて処理できない」、「検証ツールのCPUへの負荷が高い」は、検証の範囲を限定するといったノウハウを蓄積してきた。
続きは日経コンピュータ2006年7月24日号をお読み下さい。この号のご購入はバックナンバーをご利用ください。
