(57)【特許請求の範囲】
【請求項１】
ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証をコンピュータに実行させるソフトウェア検証プログラムであって、
共有変数と共有関数のうちのいずれか一方または両方が定義され、該定義された箇所それぞれにアサーションとして条件式が挿入されたライブラリと、前記共有変数と前記共有関数のうちのいずれか一方または両方を利用しているプログラムとを記憶部から取得し、該プログラムから、前記共有変数または前記共有関数を、前記プログラムの動作が並行動作または並列動作となる区間と逐次動作となる区間とに分けて前記区間毎に抽出する抽出ステップと、
前記抽出ステップにより抽出された共有変数または共有関数が定義された箇所に挿入されている前記ライブラリ内の前記条件式を評価することで、前記プログラムの前記共有変数、前記共有関数を利用している箇所がスレッドセーフ条件を満足するか否かの検証を行う条件検証ステップと
をコンピュータに実行させるソフトウェア検証プログラム。
【請求項２】
請求項１に記載のソフトウェア検証プログラムにおいて、
前記条件検証ステップは、前記共有変数と前記共有関数の全てが前記スレッドセーフ条件を満足する場合、前記プログラム中の前記共有変数と前記共有関数以外についてのスレッドセーフ検証を行うことを特徴とするソフトウェア検証プログラム。
【請求項３】
ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証を行うソフトウェア検証装置であって、
共有変数と共有関数のうちのいずれか一方または両方が定義され、該定義された箇所それぞれにアサーションとして条件式が挿入されたライブラリと、前記共有変数と前記共有関数のうちのいずれか一方または両方を利用しているプログラムとを記憶部から取得し、該プログラムから、前記共有変数または前記共有関数を、前記プログラムの動作が並行動作または並列動作となる区間と逐次動作となる区間とに分けて前記区間毎に抽出する抽出部と、
前記抽出部により抽出された共有変数または共有関数が定義された箇所に挿入されている前記ライブラリ内の前記条件式を評価することで、前記プログラムの前記共有変数、前記共有関数を利用している箇所がスレッドセーフ条件を満足するか否かの検証を行う条件検証部と
を有するソフトウェア検証装置。
【請求項４】
ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証を行うソフトウェア検証方法であって、
コンピュータが、
共有変数と共有関数のうちのいずれか一方または両方が定義され、該定義された箇所それぞれにアサーションとして条件式が挿入されたライブラリと、前記共有変数と前記共有関数のうちのいずれか一方または両方を利用しているプログラムとを記憶部から取得し、該プログラムから、前記共有変数または前記共有関数を、前記プログラムの動作が並行動作または並列動作となる区間と逐次動作となる区間とに分けて前記区間毎に抽出する抽出ステップと、
前記抽出ステップにより抽出された共有変数または共有関数が定義された箇所に挿入されている前記ライブラリ内の前記条件式を評価することで、前記プログラムの前記共有変数、前記共有関数を利用している箇所がスレッドセーフ条件を満足するか否かの検証を行う条件検証ステップと
を実行するソフトウェア検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、並行・並列ソフトウェアの検証を行うソフトウェア検証プログラム、ソフトウェア検証装置、ソフトウェア検証方法に関するものである。
【背景技術】
【０００２】
コンピュータソフトウェアの大規模化や複雑化の問題に対処するために、基本的な機能が実装され、再利用できるライブラリがソフトウェア開発者に提供されるようになった。今日では、ライブラリがソフトウェア開発（組み込み用システムから大型システムのアプリケーションまで）に必要不可欠になっている。
【０００３】
また、ハードウェアの上で並行・並列に動作するソフトウェアが必要とされてきている。そこで、開発者は、並行・並列ソフトウェア特有の不具合（データ競合およびデッドロック）の有無を検証する必要がある。並行・並列ソフトウェアに組み込み可能なライブラリを提供するためには、並行・並列動作を意識してスレッドセーフなライブラリを設計する必要がある（スレッドセーフ設計）。スレッドセーフなライブラリとは、データ競合及びデッドロックが発生しないライブラリである。スレッドセーフ設計を実現するために、ライブラリの実装においてＭＵＴＥＸロック等の同期機構が使われる。
【０００４】
しかし、同期機構を多用すると、逐次実行される部分が増えるため、性能の観点から望ましくない。そのため、ライブラリ開発者は、一部の同期機構を緩和して性能向上を図ることがある。
【０００５】
なお、本発明の関連ある従来技術として、並行・並列プログラムのテストの実施方法がある（例えば、特許文献１参照）。
【特許文献１】特表平８−５０２３７５号公報
【発明の開示】
【発明が解決しようとする課題】
【０００６】
しかしながら、同期機構を緩和したライブラリは、スレッドセーフではないため、このようなライブラリを組み込んだ並行・並列プログラムを検証する際、新たに設計した部分のみならず、ライブラリを含めたソフトウェア全体の検証が必要になる。一般的に、並行・並列ソフトウェアのスレッドセーフ検証は、コスト（時間）がかかる。特にソフトウェアの実装において複数のライブラリを利用した場合の検証コストは、非常に高くなる。
【０００７】
ライブラリを含めた並行・並列ソフトウェアの検証のためには、以下の検証技術が存在する。
【０００８】
第１の検証技術として、ツールベンダーにより提供され、並行・並列プログラム特有の不具合を検出するデバッガ等のツールを用いるテスト技術が普及している。このツールは、基本的にソフトウェアの実行時に行われる全てのメモリアクセスを記録し、共有変数にアクセスするパターンからデータ競合を検出することができる。また、このツールは、デバッガがある状態に停滞し、そこから遷移しない事象を検出することでデッドロックを洗い出すことができる。しかし、不具合を出すためのテストパターンの作成が困難である。また、十分なテストパターンを流すために必要な検証時間は非常に長く、効率は悪い。
【０００９】
第２の検証技術として、モデルチェック技術がある。モデルチェック技術は、データ競合やデッドロックが起こる可能性を網羅的に確認できる。上述したテスト技術と比較して、テストパターンは、必要ない。しかし、モデルチェック技術は、対象のサイズに対するスケーラビリティが悪く、対象とするソフトウェアの規模によっては、処理時間や必要なメモリリソースが異常に増加することがある。従って、大規模ソフトウェアとその中に含まれるライブラリの形式的検証の効率は、非常に悪い。
【００１０】
本発明は上述した問題点を解決するためになされたものであり、並行・並列ソフトウェアの検証コストを低減するソフトウェア検証プログラム、ソフトウェア検証装置、ソフトウェア検証方法を提供することを目的とする。
【課題を解決するための手段】
【００１１】
上述した課題を解決するため、本発明は、ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証をコンピュータに実行させるソフトウェア検証プログラムであって、前記ライブラリ中で定義された要素であって前記プログラムが利用できる要素である共有要素が、前記プログラム中で利用されている箇所を共有要素利用箇所として抽出する共有要素利用箇所抽出ステップと、前記ライブラリ中で前記共有要素毎に定義されたスレッドセーフ条件に基づいて、前記共有要素利用箇所抽出ステップにより抽出された共有要素利用箇所における共有要素がスレッドセーフ条件を満足するか否かの検証を行う条件検証ステップとをコンピュータに実行させるものである。
【００１２】
また、本発明に係るソフトウェア検証プログラムにおいて、前記条件検証ステップは、前記プログラム中の前記共有要素利用箇所における共有要素の全てが前記スレッドセーフ条件を満足する場合、前記プログラム中の前記共有要素利用箇所以外についてのスレッドセーフ検証を行うことを特徴とするものである。
【００１３】
また、本発明に係るソフトウェア検証プログラムにおいて、前記スレッドセーフ条件は、前記ライブラリにおいて前記共有要素に対応するアノテーションとして記述されることを特徴とするものである。
【００１４】
また、本発明に係るソフトウェア検証プログラムにおいて、前記共有要素は、前記ライブラリにより提供される共有変数と関数であることを特徴とするものである。
【００１５】
また、本発明に係るソフトウェア検証プログラムにおいて、前記スレッドセーフ条件は、前記ライブラリに対するスレッドセーフ検証によりスレッドセーフでないと判断された共有要素についてのスレッドセーフ検証結果に基づいて定義されることを特徴とするものである。
【００１６】
また、本発明に係るソフトウェア検証プログラムにおいて、前記スレッドセーフ条件は更に、前記ライブラリの仕様に基づいて定義されることを特徴とするものである。
【００１７】
また、本発明に係るソフトウェア検証プログラムにおいて、前記共有要素利用箇所抽出ステップは、前記プログラムの制御フロー解析に基づいて、前記プログラムを並行動作または並列動作を行う区間と逐次動作を行う区間に分け、前記区間毎に前記共有要素利用箇所を抽出することを特徴とするものである。
【００１８】
また、本発明は、ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証を行うソフトウェア検証装置であって、前記ライブラリ中で定義された要素であって前記プログラムが利用できる要素である共有要素が、前記プログラム中で利用されている箇所を共有要素利用箇所として抽出する共有要素利用箇所抽出部と、前記ライブラリ中で前記共有要素毎に定義されたスレッドセーフ条件に基づいて、前記共有要素利用箇所抽出部により抽出された共有要素利用箇所における共有要素がスレッドセーフ条件を満足するか否かの検証を行う条件検証部とを備えたものである。
【００１９】
また、本発明に係るソフトウェア検証装置において、前記条件検証部は、前記プログラム中の前記共有要素利用箇所における共有要素の全てが前記スレッドセーフ条件を満足する場合、前記プログラム中の前記共有要素利用箇所以外についてのスレッドセーフ検証を行うことを特徴とするものである。
【００２０】
また、本発明に係るソフトウェア検証装置において、前記スレッドセーフ条件は、前記ライブラリにおいて前記共有要素に対応するアノテーションとして記述されることを特徴とするものである。
【００２１】
また、本発明に係るソフトウェア検証装置において、前記共有要素は、前記ライブラリにより提供される共有変数と関数であることを特徴とするものである。
【００２２】
また、本発明に係るソフトウェア検証装置において、前記スレッドセーフ条件は、前記ライブラリに対するスレッドセーフ検証によりスレッドセーフでないと判断された共有要素についてのスレッドセーフ検証結果に基づいて定義されることを特徴とするものである。
【００２３】
また、本発明に係るソフトウェア検証装置において、前記スレッドセーフ条件は更に、前記ライブラリの仕様に基づいて定義されることを特徴とするものである。
【００２４】
また、本発明に係るソフトウェア検証装置において、前記共有要素利用箇所抽出部は、前記プログラムの制御フロー解析に基づいて、前記プログラムを並行動作または並列動作を行う区間と逐次動作を行う区間に分け、前記区間毎に前記共有要素利用箇所を抽出することを特徴とするものである。
【００２５】
また、本発明は、ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証を行うソフトウェア検証方法であって、前記ライブラリ中で定義された要素であって前記プログラムが利用できる要素である共有要素が、前記プログラム中で利用されている箇所を共有要素利用箇所として抽出する共有要素利用箇所抽出ステップと、前記ライブラリ中で前記共有要素毎に定義されたスレッドセーフ条件に基づいて、前記共有要素利用箇所抽出ステップにより抽出された共有要素利用箇所における共有要素がスレッドセーフ条件を満足するか否かの検証を行う条件検証ステップとを実行するものである。
【発明の効果】
【００２６】
本発明によれば、並行・並列ソフトウェアの検証コストを低減することができる。
【発明を実施するための最良の形態】
【００２７】
以下、本発明の実施の形態について図面を参照しつつ説明する。
【００２８】
まず、本実施の形態に係るプログラム検証装置の構成について説明する。
【００２９】
図１は、本実施の形態に係るプログラム検証装置の構成の一例を示すブロック図である。このプログラム検証装置は、ライブラリ１１、アノテーション付加部１２、仕様書１３、ライブラリ２１、プログラム２２、プログラム検証部２３を備える。ライブラリ１１は、プログラム２２から利用できる要素である共有変数、関数（メソッド）を含む。仕様書１３は、ライブラリ１１の仕様書の情報である。プログラム２２は、ライブラリ１１またはライブラリ２１を利用する並行・並列プログラムである。ここで、ライブラリ１１において、プログラム２２から利用できる要素を共有要素と呼ぶ。
【００３０】
次に、並列・並行プログラムの開発フローについて説明する。
【００３１】
図２は、本実施の形態に係るアノテーション付加処理の動作の一例を示すフローチャートである。まず、アノテーション付加部１２がアノテーション付加処理（アノテーション付加ステップ）を行うことにより、ライブラリ開発者により作成されたライブラリ１１にアノテーション（検証情報）を付加したライブラリ２１を生成する（Ｓ１２）。次に、プログラム検証部２３は、プログラム開発者により作成されたプログラム２２とライブラリ２１に対してプログラム検証処理を行い（Ｓ１４）、プログラム検証処理の結果プログラム２２がスレッドセーフであるか否かの判断を行う（Ｓ１６）。スレッドセーフでない場合（Ｓ１６，Ｎ）、プログラム開発者によるプログラム２２の修正が行われ（Ｓ１８）、処理Ｓ１４へ戻る。一方、スレッドセーフである場合（Ｓ１６，Ｙ）、このフローを終了する。
【００３２】
次に、アノテーション付加処理について説明する。
【００３３】
ライブラリ１１において、アノテーション付加処理によりアノテーションが付加される対象を、対象変数と対象関数とする。対象変数は、ライブラリ１１が組み込まれるプログラム２２から見える共有変数であり、対象関数は、ライブラリ１１が組み込まれるプログラム２２から呼び出せる関数である。また、アノテーションは、対象変数と対象関数に関して、並行・並列動作したときにスレッドセーフ動作を行うための必要十分条件である。
【００３４】
図３は、本実施の形態に係るアノテーション付加処理の動作の一例を示すフローチャートである。まず、アノテーション付加部１２は、ライブラリ１１のスレッドセーフ検証処理を行う（Ｓ２２）。このスレッドセーフ検証処理は、上述した対象変数と対象関数を検証対象とし、従来のルールベースチェッカ、モデルチェック技術、シミュレーション技術などを用いる。また、スレッドセーフ検証結果として、ライブラリ１１中のスレッドセーフでない位置（行番号）、理由、条件が出力される。次に、アノテーション付加部１２は、スレッドセーフ検証結果をスレッドセーフであるための条件（制約）であるスレッドセーフ条件に変換する（Ｓ２４）。次に、アノテーション付加部１２は、スレッドセーフ条件をアノテーションとしてライブラリ１１に付加し、その結果をライブラリ２１として出力し（Ｓ２６）、このフローを終了する。
【００３５】
処理Ｓ２４において、スレッドセーフ検証結果だけでは機械的にスレッドセーフ条件を導き出すことができない場合、スレッドセーフ検証結果に仕様書１３の情報を加えてスレッドセーフ条件に変換する。または、ライブラリ開発者がスレッドセーフ検証結果と仕様書１３とに基づいてスレッドセーフ条件を作成する。
【００３６】
ここで、処理Ｓ２２のスレッドセーフ検証処理において、ルールベースチェッカを用いる例について説明する。まず、ルールの内容の例を以下に示す。
【００３７】
ルールの内容：
変数Ｖａｒが共有変数、かつ、型がｆｉｎａｌでなかった場合、変数の読み出し・書き込み時に変数Ｖａｒがロックを獲得していなければならない、または、読み出し・書き込みが行われるメソッドがロックを獲得していなければならない
【００３８】
ここで、共有変数であるか否かは、ｉｓＳｈａｒｅｄで確認することができる。型は、ｍｏｄｉｆｉｅｒで確認することができる。変数の読み出しは、ｒｅａｄＡｃｃｅｓｓであり、変数の書き込みは、ｗｒｉｔｅＡｃｃｅｓｓである。変数Ｖａｒがロックを獲得したか否かは、ｈｏｌｄｓＬｏｃｋ（Ｖａｒ）で確認することができる。メソッドｔｈｉｓがロックを獲得したか否かは、ｈｏｌｄｓＬｏｃｋ（ｔｈｉｓ）で確認することができる。これらを用いると、上述したルールの内容に対するルールの記述は以下のようになる。ｈｏｌｄｓＬｏｃｋメソッドは、値がｔｒｕｅであればロックを獲得していることを表す。
【００３９】
ルールの記述：
ｉｆ  （ｉｓＳｈａｒｅｄ（Ｖａｒ）  ＆＆  ｍｏｄｉｆｉｅｒ（Ｖａｒ）  ！＝  “ｆｉｎａｌ”）  ｔｈｅｎ  ｒｅａｄＡｃｃｅｓｓ（ｈｏｌｄｓＬｏｃｋ（Ｖａｒ）  ｏｒ  Ｔｈｒｅａｄ．ｈｏｌｄｓＬｏｃｋ（ｔｈｉｓ））  ；
ｉｆ  （ｉｓＳｈａｒｅｄ（Ｖａｒ）  ＆＆  ｍｏｄｉｆｉｅｒ（Ｖａｒ）  ！＝  “ｆｉｎａｌ”）  ｔｈｅｎ  ｗｒｉｔｅＡｃｃｅｓｓ（ｈｏｌｄｓＬｏｃｋ（Ｖａｒ）  ｏｒ  Ｔｈｒｅａｄ．ｈｏｌｄｓＬｏｃｋ（ｔｈｉｓ））  ；
【００４０】
また、処理Ｓ２４におけるスレッドセーフ条件の記述は、例えば、処理Ｓ２２のルールベースチェッカから得られるルールの記述に、並行・並列動作または逐次動作を表す構文を追加し、拡張したものをスレッドセーフ条件の記述方法とする。以下に拡張の例を示す。
【００４１】
ａｓｓｅｒｔ  ｉｆＣｏｎｃｕｒｒｅｎｔ（Ｔｈｒｅａｄ．ｈｏｌｄｓＬｏｃｋ（ｔｈｉｓ））；
ａｓｓｅｒｔ  ｉｆＳｅｒｉａｌ（ｆｌａｇ  ＝＝  ｆａｌｓｅ）；
【００４２】
ここで、ｉｆＣｏｎｃｕｒｒｅｎｔ（条件式）を用いると、条件式はアサーションが含まれるメソッドが並行並列動作しているときのみ評価される。また、ｉｆＳｅｒｉａｌ（条件式）を用いると、条件式はアサーションが含まれるメソッドが逐次動作しているときのみ評価される。
【００４３】
このアノテーション付加処理によれば、スレッドセーフ条件をアノテーションとしてライブラリ２１に含めることにより、ライブラリ２１を利用するプログラム２２のスレッドセーフ検証のコストが低減される。また、仕様の情報をスレッドセーフ条件に含めることにより、適切な条件でスレッドセーフ検証を行うことができるとともに、プログラム２２のスレッドセーフ検証のコストが更に低減される。
【００４４】
次に、プログラム検証処理について説明する。
【００４５】
図４は、本実施の形態に係るプログラム検証処理の動作の一例を示すフローチャートである。まず、プログラム検証部２３は、プログラム２２のソースコード上でライブラリ２１中の共有変数やメソッドを利用している箇所（共有要素利用箇所）について、対応するアノテーションの条件を検証するアノテーション検証処理を行い（Ｓ３１）、プログラム２２が検証の結果、全てのアノテーションの条件を満足しているか否かの判断を行う（Ｓ３２）。満足していない場合（Ｓ３２，Ｎ）、プログラム検証部２３は、検証結果（アノテーションの条件を満足していない位置と内容）の表示を行い（Ｓ３３）、このフローを終了する。一方、満足している場合（Ｓ３２，Ｙ）、プログラム検証部２３は、プログラム２２のソースコード上でライブラリ２１中の共有変数やメソッド以外の共有変数とロックに着目したスレッドセーフ検証処理を行い（Ｓ３４）、全ての共有変数とロックがスレッドセーフの条件を満足しているか否かの判断を行う（Ｓ３５）。ここで、処理Ｓ３４のスレッドセーフ検証処理は、処理Ｓ２２と同様、従来のルールベースチェッカ、モデルチェック技術、シミュレーション技術などを用いる。
【００４６】
満足していない場合（Ｓ３５，Ｎ）、プログラム検証部２３は、検証結果（スレッドセーフの条件を満足していない位置と内容）の表示を行い（Ｓ３６）、このフローを終了する。一方、満足している場合（Ｓ３５，Ｙ）、つまり、プログラム２２がスレッドセーフであると判断した場合、このフローを終了する。
【００４７】
このプログラム検証処理によれば、プログラム２２のうち、ライブラリ２１に関係のある変数や関数は、アノテーションの条件の判定により容易にスレッドセーフ検証を行うことができる。また、ライブラリ２１に関係のない変数や関数だけについて、従来と同様のスレッドセーフ検証を行うことにより、スレッドセーフ検証コストを大幅に削減することができる。
【００４８】
次に、処理Ｓ３１のアノテーション検証処理について説明する。
【００４９】
図５は、本実施の形態に係るアノテーション検証処理の動作の一例を示すフローチャートである。まず、プログラム検証部２３は、プログラム２２の制御フローを解析し、並行・並列動作を行う区間とそうではない逐次動作の区間に分ける（Ｓ４１）。次に、プログラム検証部２３は、区間毎に、ライブラリ２１が提供する変数、メソッドを抽出する（Ｓ４２）。次に、プログラム検証部２３は、抽出した変数、メソッドについてアノテーションの条件を検証し（Ｓ４３）、このフローを終了し、処理Ｓ３２を実行する。
【００５０】
また、処理Ｓ３３において、プログラム検証部２３は、アノテーションの条件を満足しない変数またはメソッドがライブラリ２１とプログラム２２に出現する位置、アノテーションの内容を表示する。
【００５１】
このアノテーション検証処理によれば、並行・並列動作を行う区間と逐次動作を行う区間に分け、ライブラリ２１が提供する変数やメソッドを抽出することにより、アノテーションの条件に対して、並行・並列動作時の判定と逐次動作時の判定を適切に行うことができる。
【００５２】
本実施の形態によれば、プログラム２２の開発時には、ライブラリ２１のスレッドセーフ検証を行う必要はなく、プログラム２２のスレッドセーフ検証を行うだけで良いため、プログラム２２の開発時における検証の時間が大幅に削減され、プログラム２２の開発効率が向上する。
【００５３】
次に、Ｊａｖａ（商標）言語により記述されたライブラリ１１の具体例を用いて、アノテーション付加処理について説明する。
【００５４】
まず、第１の具体例におけるアノテーション付加処理について説明する。
【００５５】
図６は、本実施の形態に係る第１の具体例におけるライブラリ１１を示すソースコードである。ライブラリ１１には、クラスＬ１が定義されている。Ｌ１における変数ｓｈａｒｅｄ１と変数ｃｏｎｓｔは、共にｐｕｂｌｉｃ宣言されているため、Ｌ１を利用するプログラム２２からアクセス可能（自由に参照、代入できる）である。
【００５６】
並行・並列プログラムであるプログラム２２がｓｈａｒｅｄ１の参照代入を行う場合、必ず同期機構（例えば、モニター）を介して行わなければならない。一方、ｃｏｎｓｔは、ｆｉｎａｌ宣言されている。Ｊａｖａ言語において、ｆｉｎａｌ宣言された変数は、１度値が定義された後の値の変更は不可能であり、定数と同様、全てのアクセスは値の参照になる。このため、プログラム２２がｃｏｎｓｔを利用する場合、ロック等の同期機構の必要はない。
【００５７】
従って、アノテーション付加処理により付加されるアノテーションは、以下のようになる。
【００５８】
ｓｈａｒｅｄ１：利用されるプログラムにおいて、参照・代入時にロックで保護されなければならない。
ｃｏｎｓｔ：条件はない。
【００５９】
次に、第２の具体例におけるアノテーション付加処理について説明する。
【００６０】
図７は、本実施の形態に係る第２の具体例におけるライブラリ１１を示すソースコードである。ライブラリ１１には、クラスＬ２が定義されている。Ｌ２においては、変数ｓｈａｒｅｄ２、メソッドｍｅｔｈｏｄ１、メソッドｍｅｔｈｏｄ２が定義されている。ｓｈａｒｅｄ２は、Ｌ２内で共有されているが、ｐｒｉｖａｔｅ宣言されているため、Ｌ２を利用するプログラム２２から見えない。従って、ｓｈａｒｅｄ２に対するアノテーションを付加する必要はない。
【００６１】
一方、ｍｅｔｈｏｄ１とｍｅｔｈｏｄ２は、ｐｕｂｌｉｃ宣言されているため、Ｌ２を利用するプログラム２２から呼び出し可能である。ｍｅｔｈｏｄ１とｍｅｔｈｏｄ２は、Ｌ２内で共有する変数ｓｈａｒｅｄ２を参照し、代入する。それぞれのメソッドがスレッドセーフであるためにはｓｈａｒｅｄ２を参照・代入するときにロックをしなければならない。ｍｅｔｈｏｄ２はｓｙｎｃｈｒｏｎｉｚｅｄ宣言されている。Ｊａｖａ言語において、ｓｙｎｃｈｒｏｎｉｚｅｄ宣言されたメソッドは、クラス（Ｌ２）に対してロックを獲得してから共有変数（ｓｈａｒｅｄ２）へアクセスする。一方、ｍｅｔｈｏｄ１はｓｙｎｃｈｒｏｎｉｚｅｄ宣言されていないため、並行・並列動作時にデータ競合が起こる可能性がある。この具体例は、処理Ｓ２２において従来技術のルールベースチェックまたはモデルチェック技術等の静的解析を用いることで容易に解析できる。
【００６２】
従って、アノテーション付加処理により付加されるアノテーションは、以下のようになる。
【００６３】
ｓｈａｒｅｄ２：条件はない。
ｍｅｔｈｏｄ１：Ｌ２のロックを獲得した上で、このメソッドが呼び出されなければならない。
ｍｅｔｈｏｄ２：条件はない。
【００６４】
次に、第３の具体例におけるアノテーション付加処理について説明する。
【００６５】
図８は、本実施の形態に係る第３の具体例におけるライブラリ１１を示すソースコードである。ライブラリ１１には、クラスＬ３が定義されている。Ｌ３は、３つの変数（ｓｈａｒｅｄ３，Ｌ，ｃｏｎｄ）と３つのメソッド（ｉｎｉｔ，ｍｅｔｈｏｄ１，ｍｅｔｈｏｄ２）を提供しており、仕様は次の通りである。
【００６６】
・ｉｎｉｔは、初期化のとき一回しか実行されない。初期化時は並行・並列動作してはいけない。
・ｃｏｎｄの値は、並行・並列動作する場合は必ずｆａｌｓｅである。値がｔｒｕｅの場合は逐次動作が保証される。
【００６７】
ｓｈａｒｅｄ３は、ｐｒｉｖａｔｅと宣言されておりＬ３を利用するプログラム２２から見えないため、ｓｈａｒｅｄ３に対するアノテーションを付加する必要はない。Ｌ及びｃｏｎｄはｓｈａｒｅｄ３と同様にｐｒｉｖａｔｅ宣言されており、アノテーションを付加する必要はない。ｉｎｉｔ，ｍｅｔｈｏｄ１，ｍｅｔｈｏｄ２は、それぞれＬ３で共有される変数を参照、代入している。機械的にスレッドセーフ検証（例えば、ルールベースチェック、モデルチェック技術等）を行えばメソッドｍｅｔｈｏｄ１のみがスレッドセーフと判断され、メソッドｉｎｉｔとｍｅｔｈｏｄ２はスレッドセーフではないと判断される。
【００６８】
従って、スレッドセーフ検証結果だけを利用して、機械的にメソッドｉｎｉｔとｍｅｔｈｏｄ２にアノテーションを付加した場合、次のとおりになる。
【００６９】
ｉｎｉｔ：Ｌ３のロックを獲得した上で呼び出されなければならない。
ｍｅｔｈｏｄ１：条件はない。
ｍｅｔｈｏｄ２：ｃｏｎｄがｔｒｕｅの場合、Ｌ３のロックを獲得した上で呼び出されなければならない。
【００７０】
しかし、上述したＬ３の仕様からｉｎｉｔは並行・並列動作していないときに一回だけ実行されることから、アノテーションにはメソッド呼び出し時の条件としてこの仕様を付加する。また、ｍｅｔｈｏｄ２において、ｃｏｎｄがｔｒｕｅの場合、ｓｈａｒｅｄ３は同期機構を使わず（この場合はｓｙｎｃｈｒｏｎｉｚｅｄブロック）参照、及び代入されている。しかし、Ｌ３の仕様からｃｏｎｄ
の値がｔｒｕｅの場合は逐次動作が保証される。仕様の情報からメソッドｍｅｔｈｏｄ２はスレッドセーフであると容易に導き出せる。
【００７１】
従って、スレッドセーフ検証結果に加えてＬ３の仕様を用いた適切なアノテーションは次のようになる。
【００７２】
ｉｎｉｔ：メソッド呼び出し時は並行・並列動作をしていない、かつ、１回しか呼び出してはいけない。
ｍｅｔｈｏｄ１：条件はない。
ｍｅｔｈｏｄ２：条件はない。
【００７３】
この例のように、クラスの仕様書からの情報を考慮する必要がある場合は、従来のスレッドセーフ検証結果から機械的に導く出した条件のみで適切なアノテーションを付加することはできない。このようなケースでは、アノテーション付加部１２が仕様書の情報をアノテーションに付加する。または、ライブラリ開発者が仕様書に基づいて付加する。
【００７４】
次に、上述したライブラリ１１の具体例に対応するプログラム２２の具体例を用いて、プログラム検証処理について説明する。
【００７５】
まず、上述した第１の具体例におけるプログラム検証処理について説明する。
【００７６】
図９は、本実施の形態に係る第１の具体例におけるプログラム２２を示すソースコードである。このプログラム２２には、クラスＰ１が定義されている。Ｐ１は、第１の具体例により生成されたライブラリ２１（クラスＬ１）を利用する。Ｐ１の仕様は、次の通りである。
【００７７】
・メソッドｍｅｔｈｏｄ１，ｍｅｔｈｏｄ２は、並行動作する。
【００７８】
Ｐ１内のＬ１が提供する変数とメソッドに着目すると、ｍｅｔｈｏｄ１ではｃｏｎｓｔが参照され（ｒｅｆ１）、ｍｅｔｈｏｄ２ではｓｈａｒｅｄ１が参照される（ｒｅｆ２）。
【００７９】
ｃｏｎｓｔのアノテーションは“条件なし”であるため、プログラム２２のＰ１がスレッドセーフ動作するための条件は満たされている。一方、ｓｈａｒｅｄ１についてのアノテーションによれば、Ｐ１がスレッドセーフ動作するためにはアクセスする際にロックを獲得する必要がある。この条件が満たされていないことは、アサーションを使ったシミュレーションにより容易に判定される。
【００８０】
ここで、ロックの獲得をチェックするアサーション記述は、次のようになる。
【００８１】
ａｓｓｅｒｔ  Ｔｈｒｅａｄ．ｈｏｌｄｓＬｏｃｋ（ｔｈｉｓ）；
【００８２】
このアサーション記述は、アサーション記述が含まれるメソッド（この例ではｔｈｉｓで表す）がロックを獲得していなければならないことを表す。
【００８３】
従って、プログラム検証部２３は、プログラム検証処理の結果、プログラム２２がスレッドセーフでないと判定し、ｓｈａｒｅｄ１にアクセスする位置（ｒｅｆ２）の情報とｓｈａｒｅｄ１についてのアノテーションの情報を表示し、プログラム開発者にプログラム２２の修正を促す。
【００８４】
次に、上述した第２の具体例におけるプログラム検証処理について説明する。
【００８５】
図１０は、本実施の形態に係る第２の具体例におけるプログラム２２を示すソースコードである。このプログラム２２には、クラスＰ２が定義されている。Ｐ２は、第２の具体例により生成されたライブラリ２１（クラスＬ２）を利用する。Ｐ２内のＬ２が提供するメソッドに着目すると、ｒｕｎメソッドではｍｅｔｈｏｄ２が呼び出され（ｒｅｆ１）、ｍａｉｎメソッドではｍｅｔｈｏｄ１が呼び出されている（ｒｅｆ２）。
【００８６】
Ｊａｖａ言語ではｒｕｎメソッドは特別なメソッドであり、ｓｔａｒｔメソッドを呼び出すことによってスレッドが１本起動する。すなわち、ｒｕｎメソッドが呼び出されたとき並行・並列スレッドが起動する。ここで、ｍｅｔｈｏｄ２のアノテーションは“条件なし”であるため、プログラムＰ２でｍｅｔｈｏｄ２がスレッドセーフ動作するための条件は満たされている。
【００８７】
一方、ｍｅｔｈｏｄ１は、ｍａｉｎメソッド内でクラスＬ２をロックせず呼び出されている。処理Ｓ４１におけるＰ２の制御フロー解析の結果、Ｐ２は、ｍａｉｎメソッドの開始からｒｅｆ３まで逐次動作を行い、ｓｔａｒｔメソッドの呼び出し（ｒｅｆ４）から並行動作を開始する。ｍｅｔｈｏｄ１は逐次動作区間で呼び出されるため、並行・並列動作する際の条件であるアノテーションの条件は該当しない。従って、Ｐ２がＬ２のロックを獲得せずにｍｅｔｈｏｄ１を呼び出してもデータ競合・デッドロックは起きない。
【００８８】
従って、プログラム検証部２３は、プログラム検証処理の結果、プログラム２２がスレッドセーフであると判定する。
【００８９】
次に、上述した第３の具体例におけるプログラム検証処理について説明する。
【００９０】
図１１は、本実施の形態に係る第３の具体例におけるプログラム２２を示すソースコードである。このプログラム２２には、クラスＰ３が定義されている。Ｐ３は、第３の具体例により生成されたライブラリ２１（クラスＬ３）を利用する。Ｐ３内のＬ３が提供するメソッドに着目するとｒｕｎメソッドではｍｅｔｈｏｄ２が呼び出され（ｒｅｆ１）、ｍａｉｎメソッドではｉｎｉｔが呼び出される。
【００９１】
Ｌ３が提供するｍｅｔｈｏｄ１はＰ３で参照されていないので、アノテーションの条件が満足しているかを検証する必要はない。Ｌ３が提供するｉｎｉｔのアノテーションの条件によれば、並行・並列動作区間からの呼び出しは禁止されている。処理Ｓ４１におけるＰ３の制御フロー解析の結果、ｍａｉｎメソッドの開始からｒｅｆ３の直前まで逐次動作を行い、ｒｅｆ３以降は並行・並列動作を行うことが容易に分かる。更に、ｉｎｉｔは並行・並列動作区間から呼び出されていることが容易に分かる。従って、ｉｎｉｔはアノテーションの条件を満足していない。
【００９２】
一方、ｍｅｔｈｏｄ２のアノテーションは“条件なし”であるため、Ｐ３でｍｅｔｈｏｄ２がスレッドセーフ動作するための条件は満たされている。
【００９３】
従って、プログラム検証部２３は、プログラム検証処理の結果、プログラム２２がスレッドセーフでないと判定し、ｉｎｉｔを呼び出す位置（ｒｅｆ２）の情報とｉｎｉｔについてのアノテーションの情報を表示し、プログラム開発者にプログラム２２の修正を促す。
【００９４】
また、本実施の形態に係るソフトウェア検証装置は、情報処理装置に容易に適用することができ、情報処理装置の性能をより高めることができる。ここで、情報処理装置には、例えばＰＣ（Personal Computer）、サーバ、ワークステーション等が含まれ得る。
【００９５】
更に、ソフトウェア検証装置を構成するコンピュータにおいて上述した各ステップを実行させるプログラムを、ソフトウェア検証プログラムとして提供することができる。上述したプログラムは、コンピュータにより読取り可能な記録媒体に記憶させることによって、ソフトウェア検証装置を構成するコンピュータに実行させることが可能となる。ここで、上記コンピュータにより読取り可能な記録媒体としては、ＲＯＭやＲＡＭ等のコンピュータに内部実装される内部記憶装置、ＣＤ−ＲＯＭやフレキシブルディスク、ＤＶＤディスク、光磁気ディスク、ＩＣカード等の可搬型記憶媒体や、コンピュータプログラムを保持するデータベース、或いは、他のコンピュータ並びにそのデータベースや、更に回線上の伝送媒体をも含むものである。
【００９６】
なお、共有要素利用箇所抽出ステップは、実施の形態における処理Ｓ４１，Ｓ４２に対応する。また、条件検証ステップは、実施の形態における処理Ｓ４３に対応する。また、共有要素利用箇所抽出部と条件検証部は、実施の形態におけるプログラム検証部２３に対応する。
【００９７】
（付記１）  ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証をコンピュータに実行させるソフトウェア検証プログラムであって、
前記ライブラリ中で定義された要素であって前記プログラムが利用できる要素である共有要素が、前記プログラム中で利用されている箇所を共有要素利用箇所として抽出する共有要素利用箇所抽出ステップと、
前記ライブラリ中で前記共有要素毎に定義されたスレッドセーフ条件に基づいて、前記共有要素利用箇所抽出ステップにより抽出された共有要素利用箇所における共有要素がスレッドセーフ条件を満足するか否かの検証を行う条件検証ステップと
をコンピュータに実行させるソフトウェア検証プログラム。
（付記２）  付記１に記載のソフトウェア検証プログラムにおいて、
前記条件検証ステップは、前記プログラム中の前記共有要素利用箇所における共有要素の全てが前記スレッドセーフ条件を満足する場合、前記プログラム中の前記共有要素利用箇所以外についてのスレッドセーフ検証を行うことを特徴とするソフトウェア検証プログラム。
（付記３）  付記１または付記２に記載のソフトウェア検証プログラムにおいて、
前記スレッドセーフ条件は、前記ライブラリにおいて前記共有要素に対応するアノテーションとして記述されることを特徴とするソフトウェア検証プログラム。
（付記４）  付記１乃至付記３のいずれかに記載のソフトウェア検証プログラムにおいて、
前記共有要素は、前記ライブラリにより提供される共有変数と関数であることを特徴とするソフトウェア検証プログラム。
（付記５）  付記１乃至付記４のいずれかに記載のソフトウェア検証プログラムにおいて、
前記スレッドセーフ条件は、前記ライブラリに対するスレッドセーフ検証によりスレッドセーフでないと判断された共有要素についてのスレッドセーフ検証結果に基づいて定義されることを特徴とするソフトウェア検証プログラム。
（付記６）  付記５に記載のソフトウェア検証プログラムにおいて、
前記スレッドセーフ条件は更に、前記ライブラリの仕様に基づいて定義されることを特徴とするソフトウェア検証プログラム。
（付記７）  付記１乃至付記６のいずれかに記載のソフトウェア検証プログラムにおいて、
前記共有要素利用箇所抽出ステップは、前記プログラムの制御フロー解析に基づいて、前記プログラムを並行動作または並列動作を行う区間と逐次動作を行う区間に分け、前記区間毎に前記共有要素利用箇所を抽出することを特徴とするソフトウェア検証プログラム。
（付記８）  ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証を行うソフトウェア検証装置であって、
前記ライブラリ中で定義された要素であって前記プログラムが利用できる要素である共有要素が、前記プログラム中で利用されている箇所を共有要素利用箇所として抽出する共有要素利用箇所抽出部と、
前記ライブラリ中で前記共有要素毎に定義されたスレッドセーフ条件に基づいて、前記共有要素利用箇所抽出部により抽出された共有要素利用箇所における共有要素がスレッドセーフ条件を満足するか否かの検証を行う条件検証部と
を備えるソフトウェア検証装置。
（付記９）  付記８に記載のソフトウェア検証装置において、
前記条件検証部は、前記プログラム中の前記共有要素利用箇所における共有要素の全てが前記スレッドセーフ条件を満足する場合、前記プログラム中の前記共有要素利用箇所以外についてのスレッドセーフ検証を行うことを特徴とするソフトウェア検証装置。
（付記１０）  付記８または付記９に記載のソフトウェア検証装置において、
前記スレッドセーフ条件は、前記ライブラリにおいて前記共有要素に対応するアノテーションとして記述されることを特徴とするソフトウェア検証装置。
（付記１１）  付記８乃至付記１０のいずれかに記載のソフトウェア検証装置において、
前記共有要素は、前記ライブラリにより提供される共有変数と関数であることを特徴とするソフトウェア検証装置。
（付記１２）  付記８乃至付記１１のいずれかに記載のソフトウェア検証装置において、
前記スレッドセーフ条件は、前記ライブラリに対するスレッドセーフ検証によりスレッドセーフでないと判断された共有要素についてのスレッドセーフ検証結果に基づいて定義されることを特徴とするソフトウェア検証装置。
（付記１３）  付記１２に記載のソフトウェア検証装置において、
前記スレッドセーフ条件は更に、前記ライブラリの仕様に基づいて定義されることを特徴とするソフトウェア検証装置。
（付記１４）  付記８乃至付記１３のいずれかに記載のソフトウェア検証装置において、
前記共有要素利用箇所抽出部は、前記プログラムの制御フロー解析に基づいて、前記プログラムを並行動作または並列動作を行う区間と逐次動作を行う区間に分け、前記区間毎に前記共有要素利用箇所を抽出することを特徴とするソフトウェア検証装置。
（付記１５）  ライブラリと該ライブラリを利用して並行動作または並列動作を行うプログラムとで構成されるソフトウェアの検証を行うソフトウェア検証方法であって、
前記ライブラリ中で定義された要素であって前記プログラムが利用できる要素である共有要素が、前記プログラム中で利用されている箇所を共有要素利用箇所として抽出する共有要素利用箇所抽出ステップと、
前記ライブラリ中で前記共有要素毎に定義されたスレッドセーフ条件に基づいて、前記共有要素利用箇所抽出ステップにより抽出された共有要素利用箇所における共有要素がスレッドセーフ条件を満足するか否かの検証を行う条件検証ステップと
を実行するソフトウェア検証方法。
（付記１６）  付記１５に記載のソフトウェア検証方法において、
前記条件検証ステップは、前記プログラム中の前記共有要素利用箇所における共有要素の全てが前記スレッドセーフ条件を満足する場合、前記プログラム中の前記共有要素利用箇所以外についてのスレッドセーフ検証を行うことを特徴とするソフトウェア検証方法。
（付記１７）  付記１５または付記１６に記載のソフトウェア検証方法において、
前記スレッドセーフ条件は、前記ライブラリにおいて前記共有要素に対応するアノテーションとして記述されることを特徴とするソフトウェア検証方法。
（付記１８）  付記１５乃至付記１７のいずれかに記載のソフトウェア検証方法において、
前記共有要素は、前記ライブラリにより提供される共有変数と関数であることを特徴とするソフトウェア検証方法。
（付記１９）  付記１５乃至付記１８のいずれかに記載のソフトウェア検証方法において、
前記スレッドセーフ条件は、前記ライブラリに対するスレッドセーフ検証によりスレッドセーフでないと判断された共有要素についてのスレッドセーフ検証結果に基づいて定義されることを特徴とするソフトウェア検証方法。
（付記２０）  付記１９に記載のソフトウェア検証方法において、
前記スレッドセーフ条件は更に、前記ライブラリの仕様に基づいて定義されることを特徴とするソフトウェア検証方法。
【図面の簡単な説明】
【００９８】
【図１】本実施の形態に係るプログラム検証装置の構成の一例を示すブロック図である。
【図２】本実施の形態に係るアノテーション付加処理の動作の一例を示すフローチャートである。
【図３】本実施の形態に係るアノテーション付加処理の動作の一例を示すフローチャートである。
【図４】本実施の形態に係るプログラム検証処理の動作の一例を示すフローチャートである。
【図５】本実施の形態に係るアノテーション検証処理の動作の一例を示すフローチャートである。
【図６】本実施の形態に係る第１の具体例におけるライブラリ１１を示すソースコードである。
【図７】本実施の形態に係る第２の具体例におけるライブラリ１１を示すソースコードである。
【図８】本実施の形態に係る第３の具体例におけるライブラリ１１を示すソースコードである。
【図９】本実施の形態に係る第１の具体例におけるプログラム２２を示すソースコードである。
【図１０】本実施の形態に係る第２の具体例におけるプログラム２２を示すソースコードである。
【図１１】本実施の形態に係る第３の具体例におけるプログラム２２を示すソースコードである。
【符号の説明】
【００９９】
１１  ライブラリ、１２  アノテーション付加部、１３  仕様書、２１  ライブラリ、２２  プログラム、２３  プログラム検証部。
【図１】
0004712583.tif 000002
【図２】
0004712583.tif 000003
【図３】
0004712583.tif 000004
【図４】
0004712583.tif 000005
【図５】
0004712583.tif 000006
【図６】
0004712583.tif 000007
【図７】
0004712583.tif 000008
【図８】
0004712583.tif 000009
【図９】
0004712583.tif 000010
【図１０】
0004712583.tif 000011
【図１１】
0004712583.tif 000012