富士通研究所がNASAのJavaプログラム検証ツールを拡張、数万行のWebアプリの自動検証に成功

　富士通研究所（本社：川崎市）と同社の米国法人は2010年1月12日、オープンソースのJavaプログラム検証ツール「Java PathFinder」を拡張し、文字列型データの自動検証に対応させる技術を開発したと発表した。従来の手作業のテストに比べて検証の網羅性を大幅に向上できるという。

　「Java PathFinder」は、ソフトウェアが正しく開発されたかを確認するプログラムの検証ツールで、米航空宇宙局（NASA）が開発した。火星探査機の制御システムの検証などに使われ、2005年にオープンソース化された。与えられたJavaプログラムのソースコードに対して具体的なテストデータを与えなくても、入力データのさまざまなバリエーションによって引き起こされる動作を自動的に実行する機能（シンボリック実行モード）を備える。

　しかし、これまで同機能には数値型のデータしか扱えないという制限があり、業務アプリケーションで利用するには、バリエーションの多い文字列型データを扱えるように拡張しなければならなかった。富士通研究所の技術は、これを実現したもので、検証の適用範囲を拡大する。

　具体的には（1）入力された文字列に関連する条件を自動的に抽出し、コンパクトな表現形式でモデル化（2）文字列のシンボリック実行機能を拡張するための共通インタフェースの開発――の2つ。シンボリック実行を効率よく行い、利用者はモデル化方式などの変更や独自の拡張ができるようになるという。実験では、Webアプリケーション数万行を検証することに成功した。

　開発した技術の一部はJava PathFinderに実装され、OSSとして公開される。

Java PathFinder
http://babelfish.arc.nasa.gov/trac/jpf

富士通研究所
http://jp.fujitsu.com/group/labs/

NASA
http://www.nasa.gov/