ソフトウェアの信頼性と安全性向上を目指すディペンダブル・ソフトウェア・フォーラムの発足について

　（株）NTTデータ、富士通（株）、日本電気（株）、（株）日立製作所、（株）東芝の5社と、大学共同利用機関法人　情報・システム研究機構　国立情報学研究所^（注1）は、本日、ディペンダブル・ソフトウェア・フォーラム（Dependable Software Forum、略称名はDSF）を発足させました。
　DSFは、障害を起こさないソフトウェアの生成を実現するために、回避（故障や攻撃の発生を予防）、除去（故障の数や攻撃の程度を減少）、耐障害性（フォールトトレラント）という3つの観点から実践的、かつ系統的・論理的な構成技術と設計技術を確立させる研究開発活動です。将来、本活動による成果をIT業界へ普及・定着させ、ソフトウェアに起因するシステム障害の低減を目指します。

【背景】

　金融、通信、医療、交通、エネルギーなど大規模かつ社会を支える重要なインフラシステムから最近注目されているクラウドコンピューティング、さらには携帯電話や情報家電などでも必ずソフトウェアが動いています。ソフトウェアは一般的には目に見えないため、その存在に気付かないことが多いものの、現代社会においてはなくてはならないものとしてその重要性はますます高まっています。そのため、ソフトウェアの不具合によるトラブルが発生した場合、個人や企業が経済的被害を受ける可能性や、社会全体の活動に重大な影響を及ぼす可能性も増しています。
　一方、ますます短縮化されるソフトウェアの開発サイクルやソフトウェア自体の大規模化・複雑化の中で、法律・社会情勢の変化による仕様変更への対応や、技術進歩へのキャッチアップなど、開発にあたる技術者の環境は日々、厳しいものになってきています。
　ディペンダブル・ソフトウェアは、主として信頼性や安全性向上を目指すソフトウェアの考え方です。現在、ディペンダブル・ソフトウェアは重要性を増すソフトウェアのあるべき姿として注目されており、米国、欧州、中国では高信頼なソフトウェア開発の応用研究に国家的な規模で戦略的に取り組んでいます。また、インドではディペンダブル・ソフトウェア等を実現するIT人材の育成に注力しております。日本においては従来、ソフトウェアを開発する企業ごとに研究を進めてきましたが、今回、5社と1機関は、共同検討による迅速な対応手段の確立と、その成果のIT業界全体への普及展開を目指すことで合意し、DSFを発足させました。

【具体的な取り組み内容について】

　DSFにおける最初の取り組みとして、ディペンダブル・ソフトウェア実現の有力な手段である形式手法に着目し、具体的な検討活動を行うタスクフォースとして、形式手法適用評価WG（Formal Method Application WG、以下FMAWG）を立ち上げます。
　形式手法とは、品質の高いソフトウェアを効率よく開発するために、数学を基盤とした矛盾のない仕様書を書いて、それが正しいかどうかを検証する手法のことです。FMAWGは、形式手法の産業界への効果的な普及と定着を目指し、形式手法に関して実績およびノウハウを持つ企業・個人・団体による有益な議論と知見の共有を行い、共同で成果物を構築することを推進します。また、実際の開発現場で有効に活用できる形式手法の適用事例や適用ノウハウを蓄積・公開し、ユーザにとってもソフトウェアの不具合が減少するなど品質向上のメリットが大きい、形式手法を適用したシステム開発の可能性を追求します。

図：DSFの検討範囲

【今後の活動について】

　FMAWGの立ち上げのほか、進捗により適宜、新しいWGを立ち上げて研究を進める予定です。DSFとしては2011年度末を目途に成果物を構築し、公開することを目指します。

【用語の説明】

ディペンダブル・ソフトウェア (Dependable Software)

　利用者が信頼・安心して利用できる、頼りになるソフトウェアであり、可用性、信頼性、安全性、機密性、完全性、保守性といった複合的要件を満足する。

• 可用性 (Availability) ：利用者がシステムを使用し続けることができる性質
• 信頼性 (Reliability) ：システムのハードウェアやソフトウェアが故障する頻度
• 安全性 (Safety) ：システムが人間や環境に危害を及ぼす度合い
• 機密性 (Confidentiality) ：アクセスを許可された者だけがシステムで管理する情報にアクセスできること
• 完全性 (Integrity) ：システムで管理する情報を保護して、正確かつ完全である（改ざんされない）こと
• 保守性 (Maintainability) ：システムが故障したときの修理のしやすさのこと

耐障害性（フォールトトレラント）

　システムの一部に障害が発生したとしても、システム全体としては停止することなく動作し続けること。

クラウドコンピューティング

　インターネット経由で様々なサービスが利用できる新しいコンピュータの利用形態の総称である。利用者はインターネット先にあるハードウェアやソフトウェア、データなどが集約されているところからサービスを受け、サービス利用料金を支払う形となる。

形式手法（フォーマルメソッド）

　数学を基盤とした正確な仕様の記述と仕様の検証などの技術を含む包括的手法の総称である。正確に仕様を記述することにより、要求や仕様の矛盾、抜け漏れ等のソフトウェア不具合に気付く。さらにツールの支援で仕様の検証をすることにより、要求や仕様の矛盾、抜け漏れ等のソフトウェア不具合を抽出することができる。

注1　（株）NTTデータ（代表取締役社長：山下　徹）、富士通（株）（代表取締役会長 兼 社長：間塚　道義）、日本電気（株）（代表取締役 執行役員社長：矢野　薫）、（株）日立製作所（代表執行役 執行役会長兼執行役社長：川村　隆）、（株）東芝（取締役 代表執行役社長：佐々木　則夫）の5社と、大学共同利用機関法人　情報・システム研究機構　国立情報学研究所（所長：坂内　正夫）