システム構築/プロジェクトマネジメント システム構築/プロジェクトマネジメント記事一覧へ

[最前線]

ソフトウェアの信頼性を根本的に高める「形式手法(Formal Method)」の本質

2011年11月7日(月)

“お絵かき”レベルの仕様策定から脱皮する ソフトウェアには自動車や機械をはじめとする他の工業製品と違った特徴がある。「柔軟さ」こそ、それだ。 ところが、柔軟性はIT活用の幅を広げやすくする一方で、ともすればシステムの信頼性や安全性を損なう一因にもなる。 特に高信頼性が求められるシステムでは、柔軟なゆえに可能な場当たり的なコード変更が致命的な障害につながりかねない。 こうした事態を避けるべく、最近にわかに関心が高まっているのが「形式手法(Formal Method)」である。 数学的な記述を伴うので取っつきにくい面はあるが、企業のIT責任者や担当者は、少なくとも本質を理解しておくべきだ。

ITが広く社会に浸透し、個人の生活や企業活動にとって不可欠な役割を担うようになって久しい。それだけにITに対する信頼性や安全性の要求は、かつてないほどに高まっている。ひとたび障害が発生すれば、多くの個人や企業に甚大な影響を及ぼすからだ。

例えば、銀行のオンラインシステムや航空機の予約システムがダウンすれば、預金の引き出しや搭乗手続き、計画通りの運航が困難になり、多数の人が影響を受ける。自動車の電子制御システムに問題が生じれば、最悪の場合、人命を危機にさらす。

このような背景から、システム稼働時の信頼性を高める様々な試みがなされている。システムを構成する機器の冗長化は、その1つ。障害から自律回復する技術の研究やシステムのダウンタイムを減らすための工夫も重ねられている。開発においても同様に、テストに莫大な工数を費やしたり、ミスやエラーを徹底的に排除したりする試みがなされている。こうした取り組みが運用や開発の工程で着々と広がるのに対し、上流の工程、すなわち仕様策定における信頼性向上の取り組みはあまり進んでいないのが実情だ。

以下では、まず信頼性の低い仕様が生まれてしまう原因を考察する。そのうえで仕様の信頼性を高める手段として注目を集め始めている「形式手法(Formal Method)」について解説する。

この記事の続きをお読みいただくには、
会員登録(無料)が必要です
登録済みの方はこちら

IT Leaders 雑誌版、電子版をご購読の方、会員登録済みの方は下記ボタンよりログインして続きをお読みください

初めての方はこちら

IT Leaders 会員になると
会員限定公開の記事を読むことができます
IT Leadersのメルマガを購読できます

【次ページ】
  • 1
  • 2
バックナンバー
最前線一覧へ
関連記事

ソフトウェアの信頼性を根本的に高める「形式手法(Formal Method)」の本質 “お絵かき”レベルの仕様策定から脱皮する ソフトウェアには自動車や機械をはじめとする他の工業製品と違った特徴がある。「柔軟さ」こそ、それだ。 ところが、柔軟性はIT活用の幅を広げやすくする一方で、ともすればシステムの信頼性や安全性を損なう一因にもなる。 特に高信頼性が求められるシステムでは、柔軟なゆえに可能な場当たり的なコード変更が致命的な障害につながりかねない。 こうした事態を避けるべく、最近にわかに関心が高まっているのが「形式手法(Formal Method)」である。 数学的な記述を伴うので取っつきにくい面はあるが、企業のIT責任者や担当者は、少なくとも本質を理解しておくべきだ。

PAGE TOP