PRESS RELEASE （技術）
2010年1月12日
Fujitsu Laboratories of America, Inc.
株式会社富士通研究所
Javaプログラムを網羅的に検証する技術を開発
文字列シンボリック実行機能をNASAが採用し、オープンソースとして公開
Fujitsu Laboratories of America, Inc.（注1） と株式会社富士通研究所（注2）（以下、富士通研究所）は、Javaプログラムで入力されるさまざまなデータに対して、プログラムの動作が仕様に合っているかを人手を介さず自動的に検証する技術を開発し、Webアプリケーション数万行を検証することに成功しました。
本技術は、米国National Aeronautics and Space Administration（注3）（以下、NASA）が開発したJavaプログラム向け検証ツールのJava PathFinderを、数値型の入力データだけでなく文字列型の入力データを効率良く扱えるように拡張したものです。
開発した技術の一部はNASAに採用され、オープンソースとして公開されます。
開発の背景
NASAは宇宙航空技術の開発の一環として、システムを制御するソフトウェアに関する研究開発を行っています。NASAのAmes Research Center（注4）では、ソフトウェアが正しく開発されたかを確認するソフトウェア検証技術の研究を行っており、その成果の一環としてJavaで記述されたプログラムの検証ツールJava PathFinderを開発しました。
この検証ツールは、火星探査機の制御システムの検証などに使われ、その成果は2005年にオープンソース化されました。機能を拡張するための共通インターフェースが整備されているため、富士通研究所をはじめとする企業や大学など多くの研究機関が、Javaの検証ツールのフレームワークとして採用してきました。
課題
プログラムの動作が仕様に合っているかどうかを検証するには、人手による莫大なテストデータの作成と長時間の検証時間が必要になります。
Java PathFinderでは、与えられたJava プログラムのソースコードに対して、具体的なテストデータを与えなくても入力データのさまざまなバリエーションにより引き起こされる動作を自動的に実行する機能（シンボリック実行モード）（注5） を提供しています。本機能は、Symbolic Java PathFinderと呼ばれ、動作条件を全て効率的に実行するテストデータの生成や、プログラムが指定されたアプリケーション仕様を満たしているかの検証を自動的に行うことができます。
しかし、従来ではJava PathFinderは数値型のデータしか扱うことができず、想定すべきバリエーションの多い文字列型データを扱うことができませんでした。業務アプリケーションでは処理対象データの多くは文字列型データであり、動作を検証するためには文字列型データへの対応が必要となっていました。
開発した新技術
富士通研究所は、上記の課題を解決するために、Java PathFinderのシンボリック実行モードで文字列を扱う技術を開発し、検証の適用範囲を拡大しました。今回開発した技術の特長は以下の通りです。
- ビジネスアプリケーションで多用される「文字列」のモデル化方式
口座番号のような数字の入力データについても、アプリケーションの中では文字列として処理され、想定外である文字記号が入力されていないか、番号の長さが仕様に合っているかなどの仕様条件の検証を行います。今回開発した技術では、入力された文字列に関連する条件を自動的に抽出し、コンパクトな表現形式でモデル化することにより、シンボリック実行を効率良く行うことができます。
- 拡張可能な共通インターフェース
文字列のシンボリック実行機能を拡張するための共通インターフェースを開発しました。これにより、Java PathFinderの利用者はモデル化方式などの変更や独自の拡張を容易に行うことができます。
図1：シンボリック実行の概要
効果
本技術により、市場の広がりによって品質への要求がますます高まっているWebアプリケーションなどのエンタープライズ系システムのソフトウェアを高い網羅性で検証できるようになりました。富士通研究所が行った実験ではJavaベースのWebアプリケーション数万行を処理することに成功し、従来の手作業のテストに比べて検証の網羅性が大幅に向上しました。
モデル検査の権威で、Association for Computing Machinery (ACM)主催の2007年A.M.Turing（チューリング）賞（注6）の受賞者の一人であるDr. Edmund Clarke（エドムンド・クラーク博士）は次のように述べています：
「NASAのオープンソースソフトウェアをベースとした富士通の開発がソフトウェア検証の分野を先行するのをみて喜ばしく思います。実用的な規模のWebベースシステムを解析する、両者のシンボリック実行やソフトウェアモデル検査および文字列解析の革新的利用はこの分野での大きな前進です。」
オープンソースとして公開
今回開発した文字列型への拡張機能はNASAのJava PathFinderの重要な拡張機能であり、共通インターフェース部分をオープンソースとして公開することで、世界中の開発者や研究者がJava PathFinderを用いた文字列シンボリック実行機能を利用したり、拡張できるようになります。さらに、本技術によって、ソフトウェア検証の技術開発が加速されることも期待されます。
今後
今後は大規模で複雑なJavaアプリケーションに対して検証をすすめ、本格的な実用化を目指します。
商標について
記載されている製品名などの固有名詞は、各社の商標または登録商標です。
以上
注釈
- 注1 Fujitsu Laboratories of America, Inc.：
- 代表取締役社長 松本均、米国カリフォルニア州。
- 注2 株式会社富士通研究所：
- 代表取締役社長 村野和雄、本社 神奈川県川崎市。
- 注3 National Aeronautics and Space Administration：
- アメリカ航空宇宙局。米国政府で宇宙開発を担当する部局。
- 注4 NASA Ames Research Center：
- Director S. Pete Worden、本社 米国カリフォルニア州。
- 注5 シンボリック実行：
- Symbolic PathFinder。
テストデータの値をシンボルとして用意し、実行時に分岐条件を元にシンボルのとり得る範囲の「場合分け」を行いながら、それぞれのパスを実行する方式。 - 注6 Turing（チューリング）賞：
- Association for Computing Machinery (ACM)主催の賞で最も名誉ある賞であり、コンピューティング分野の技術において革新的な貢献をした人物に贈られる賞。
関連リンク
本件に関するお問い合わせ
株式会社富士通研究所
ソフトウェア&ソリューション研究所 ソフトウェアイノベーション研究部
電話： 044-754-2675（直通）
E-mail： java-verification@ml.labs.fujitsu.com
プレスリリースに記載された製品の価格、仕様、サービス内容、お問い合わせ先などは、発表日現在のものです。その後予告なしに変更されることがあります。あらかじめご了承ください。