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

[市場動向]

DSF、東証のシステムで形式手法の有用性を確認

2012年4月27日(金)

要求定義や設計段階でエラーやミスの混入を防ぐには、どうすればいいか。有力な解の一つが形式手法(Formal Method)である。自動車や電子機器など他の工業製品(ハードウェア)と違って、ソフトウェアには融通無碍という特徴があり、だからこそ様々なハードをソフトで置き換える試みが進む。だがこの特徴がシステムの信頼性や安全性を損なう要因でもある。そこで数理論理学に基づく仕様記述によってこの問題を解決するのが形式手法、という因果関係だ(本誌2011年11月号「ソフトウェアの信頼性を根本的に高める「形式手法(Formal Method)」の本質」参照)。

形式手法の歴史は1970年代にさかのぼれるほど古く、日本でも大きなシステム事故が起きるたびに、注目されてきた。しかし、一向に普及する気配がない。実際、上記の本誌記事を読んでいなければ、「形式手法といわれても何のことか分からない」という人も多いだろう。

そうした中、この手法の普及/啓蒙を目指して、国立情報学研究所と国内ベンダー6社(NTTデータ、富士通、NEC、日立製作所、東芝、SCSK)が2009年に設立したディペンダブル・ソフトウェア・フォーラム(DSF)は、「情報系の実稼働システムを対象とした形式手法適用実験報告書」をまとめ、情報処理推進機構(IPA)のWebサイトで公開した。東京証券取引所の協力を得て、実際の情報システムの設計書に形式手法を適用。従来は後工程で見つかっていた問題を、基本設計の段階で発見することを実証したものだ。

具体的には、東京証券取引所の投資家向け情報配信システム(すでに開発済み)の設計書が対象。DSFは2011年8月から2012年3月にかけて、同システムのレビュー済み設計書の一部を「Event-B」、「SPIN」、「VDM++」といった形式仕様言語で記述し直して検証した。その結果、レビューをすり抜け、後工程で修正された問題点を13件検出した。

IPAソフトウェアエンジニアリングセンターの松田晃一所長は、「欠陥をテストや受け入れなど後工程でカバーするとプログラムの書き直しなどで、(上流工程で発見した場合の)30倍のコストがかかる。それを形式手法で回避できることを実証した意義は大きい」と語る。当然だが、コストがかかっても欠陥を排除できればまだいい。東証の上記のシステムの場合はなかったが、レビューやテストで欠陥を排除できない可能性もあるので、その面でも形式手法の利点は大きいと言える。

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

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

初めての方はこちら

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

関連記事

DSF、東証のシステムで形式手法の有用性を確認要求定義や設計段階でエラーやミスの混入を防ぐには、どうすればいいか。有力な解の一つが形式手法(Formal Method)である。自動車や電子機器など他の工業製品(ハードウェア)と違って、ソフトウェアには融通無碍という特徴があり、だからこそ様々なハードをソフトで置き換える試みが進む。だがこの特徴がシステムの信頼性や安全性を損なう要因でもある。そこで数理論理学に基づく仕様記述によってこの問題を解決するのが形式手法、という因果関係だ(本誌2011年11月号「ソフトウェアの信頼性を根本的に高める「形式手法(Formal Method)」の本質」参照)。

PAGE TOP