(57)【特許請求の範囲】
【請求項１】
複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証をコンピュータに実行させるプログラムの検証プログラムであって、
前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出ステップと、
前記検出ステップにより検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記第１の部分と前記第２の部分の基本ブロックをそれぞれ異なる状態に割り付け、前記制御構造部分に基づいて遷移を表すことにより、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成し、該生成したモデルを記憶部に記憶するモデル生成ステップと、
前記モデル生成ステップにより前記記憶部に記憶された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証ステップと、
をコンピュータに実行させるプログラムの検証プログラム。
【請求項２】
請求項１に記載のプログラムの検証プログラムにおいて、
前記検出ステップは、変更の影響を受ける共有変数が出現する部分と該共有変数のロックの部分を前記第１の部分とすることを特徴とするプログラムの検証プログラム。
【請求項３】
複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証を行うプログラムの検証装置であって、
前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出部と、
前記検出部により検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記第１の部分と前記第２の部分の基本ブロックをそれぞれ異なる状態に割り付け、前記制御構造部分に基づいて遷移を表すことにより、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成し、該生成したモデルを記憶部に記憶するモデル生成部と、
前記モデル生成部により前記記憶部に記憶された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証部と、
を備えてなるプログラムの検証装置。
【請求項４】
複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証を行うプログラムの検証方法であって、
前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出ステップと、
前記検出ステップにより検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記第１の部分と前記第２の部分の基本ブロックをそれぞれ異なる状態に割り付け、前記制御構造部分に基づいて遷移を表すことにより、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成し、該生成したモデルを記憶部に記憶するモデル生成ステップと、
前記モデル生成ステップにより前記記憶部に記憶された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証ステップと、
を実行するプログラムの検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、並行プログラムまたは並列プログラムの検証を行うためのプログラムの検証プログラム、プログラムの検証装置、プログラムの検証方法に関するものである。
【背景技術】
【０００２】
並行プログラムや並列プログラムは、複数のプロセス（スレッド）で構成される。これらのプロセスは、実行中に同一の共有リソース（共有変数）を参照したり、書き換えたりする。複数のプロセスによる共有リソースの自由な参照や書き換えを許すと、設計者の意図とは異なる結果がプログラムにより出力される可能性がある。
【０００３】
ここで、並列プログラムの具体例を用いて説明する。この例における並列プログラムは、共有変数ｓｈａｒｅｄの定義、関数Ｐｒｏｃｅｓｓ０１、関数Ｐｒｏｃｅｓｓ０２から構成される。図３２は、並列プログラムにおける共有変数の定義の一例を示すソースコードである。また、図３３は、並列プログラムにおける関数Ｐｒｏｃｅｓｓ０１の一例を示すソースコードである。また、図３４は、並列プログラムにおける関数Ｐｒｏｃｅｓｓ０２の一例を示すソースコードである。２つのプロセスである関数Ｐｒｏｃｅｓｓ０１、関数Ｐｒｏｃｅｓｓ０２は、共有変数ｓｈａｒｅｄを共有する。この並列プログラムは、関数Ｐｒｏｃｅｓｓ０１、関数Ｐｒｏｃｅｓｓ０２は、並列に動作し、関数ａ（１），ｂ（０）が交互に呼び出される仕様である。第１の並列プログラムのトレースの一例として、次のトレースが起こり得る。
【０００４】
１．Ｐｒｏｃｅｓｓ０１．ｓｈａｒｅｄ参照（ｓｈａｒｅｄ＝＝０）
２．Ｐｒｏｃｅｓｓ０１．ｓｈａｒｅｄ＝１
３．Ｐｒｏｃｅｓｓ０２．ｓｈａｒｅｄ参照（ｓｈａｒｅｄ＝＝１）
４．Ｐｒｏｃｅｓｓ０２．ｓｈａｒｅｄ＝０
５．Ｐｒｏｃｅｓｓ０２．ｂ（０）
６．Ｐｒｏｃｅｓｓ０１．ａ（０）
【０００５】
このトレースの例では、関数ａと関数ｂの実行順番が逆転し、引数は共に０となり、仕様を満たさないことから、不具合である。
【０００６】
このような不具合を防ぐために、ＭＵＴＥＸロックやセマフォア等の同期機構が使われる。例えば、ＭＵＴＥＸロックを使ってプログラムを修正することができる。同期機構を使うことにより、１つのプロセスが共有リソースへの参照や書き込みを行うとき、別のプロセスが干渉しないことから、設計された順番通りに逐次実行される。図３５は、並列プログラムにおける関数Ｐｒｏｃｅｓｓ０１の修正結果の一例を示すソースコードである。図３６は、並列プログラムにおける関数Ｐｒｏｃｅｓｓ０２の修正結果の一例を示すソースコードである。この例では、ロックｌに保護されている部分（ｌｏｃｋの呼び出しからｕｎｌｏｃｋの呼び出しまでの間）は、逐次実行される。
【０００７】
なお、本発明の関連ある従来技術として、例えば、下記に示す特許文献１が知られている。この並列プログラム動作解析方法は、並列計算機上で動作する並列プログラムについて、並列プログラムを構成する各プログラムの状態遷移を表示すると共に、不具合の原因の特定を支援するものである。
【特許文献１】特開平８−３２８８９７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００８】
しかしながら、上述した同期機構を多用すると逐次に実行される部分が増えることにより、プログラムの並列性が活かされず、性能の観点からは望ましくない。また、多くの場合、同期機構の実行にオーバヘッドが存在するため、性能低下の要因となる。
【０００９】
但し、多くのケースでは、並列・並行プログラムの実行には仮定が設けられる。その仮定を考慮してプログラムを変更すると、一部の同期を緩和することができる。同期を緩和した結果、プロセスが並行または並列に実行できる時間が増えて、プログラム全体の実行速度が向上する。正しく動作するように並列・並行プログラムの速度を改善するためには、変更前と変更後のプログラムの結果を比較しながら行う作業が必要であり、この作業を行うためには、デバッガのような対話的なツールが必要となる。特に、並行・並列プログラムの同期が原因となる不具合の特定は、難しい作業である。
【００１０】
通常の逐次プログラムのデバッガでは、デバッグ対象プログラムに対するテストデータを決めておき、設計者がステップ実行しながら実行結果を観測する。並行・並列プログラムにおいて、多くの場合、実行結果はテストデータに依存するだけでなく、各プロセスの共有リソースへアクセスするタイミングにも依存する。しかしながら、通常の逐次プログラム用のデバッガはタイミングを考慮していないため、並行・並列プログラムのデバッグに向いていない。
【００１１】
この問題に対して、並行・並列プログラムに特化したデバッガは存在する。このデバッガは、並行・並列に動作するプロセスの実行タイミングを変更しながら、テストデータを流す方式を採用している。しかし、プロセスのあらゆる実行タイミングを試行するため、デバッグ時間が非常に長くなってしまう。
【００１２】
また、並行・並列プログラムのデバッグには、モデルチェックを代表とする形式的検証技術が使われている。ここで、通常のモデルチェックの手順について説明する。変更前の正しく動作するプログラム全体のモデル、例えば、ＦＳＭ（Finite State Machine：有限状態機械）を予め作成する。プログラムの変更後、再度、変更後のプログラムのモデルを作成し、両方のモデルについて等価性検証等の技術を用いて比較する。しかしながら、プログラムの規模が大きい場合、モデル作成は非常に時間がかかると共に、モデルの比較も非常に時間がかかる。従って、一般的なプログラムの対話的デバッグ作業は困難であった。
【００１３】
本発明は上述した問題点を解決するためになされたものであり、並行・並列プログラムの対話的デバッグ作業を可能にするための効率的な検証を行うプログラムの検証プログラム、プログラムの検証装置、プログラムの検証方法を提供することを目的とする。
【課題を解決するための手段】
【００１４】
上述した課題を解決するため、本発明は、複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証をコンピュータに実行させるプログラムの検証プログラムであって、前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出ステップと、前記検出ステップにより検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成するモデル生成ステップと、前記モデル生成ステップにより生成された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証ステップとをコンピュータに実行させるものである。
【００１５】
また、本発明に係るプログラムの検証プログラムにおいて、前記検出ステップは、変更の影響を受ける共有変数が出現する部分と該共有変数のロックの部分を前記第１の部分とすることを特徴とするものである。
【００１６】
また、本発明に係るプログラムの検証プログラムにおいて、前記検出ステップは、前記検証対象プログラムにおいて前記第１の部分にマークを付加することを特徴とするものである。
【００１７】
また、本発明に係るプログラムの検証プログラムにおいて、前記モデル生成ステップは、前記第１の部分と前記第２の部分の基本ブロックを状態に割り付け、前記制御構造部分に基づいて遷移を表すことにより、有限状態機械をモデルとして生成することを特徴とするものである。
【００１８】
また、本発明に係るプログラムの検証プログラムにおいて、前記モデル生成ステップは、前記モデルにおいて、前記第１の部分を含まない複数の状態をまとめて１つの状態とすることを特徴とするものである。
【００１９】
また、本発明に係るプログラムの検証プログラムにおいて、前記検証ステップは、まず、前記変更が施された関数について変更前のモデルと変更後のモデルの比較を行い、該比較の結果が一致しない場合、前記変更が施された関数のモデルと前記変更の影響を受ける共有変数を用いた関数のモデルの状態の積で得られるモデルについて、変更前のモデルと変更後のモデルの比較を行うことにより、前記変更後の検証対象プログラムの検証を行うことを特徴とするものである。
【００２０】
また、本発明に係るプログラムの検証プログラムにおいて、前記検証ステップは、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態を表示することを特徴とするものである。
【００２１】
また、本発明に係るプログラムの検証プログラムにおいて、前記検証ステップは、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態に至る実行順序を検出し、該実行順序を表示することを特徴とするものである。
【００２２】
また、本発明に係るプログラムの検証プログラムにおいて、前記検証ステップは、ルールベースチェックまたはモデルチェックを用いて、変更後の検証対象プログラムの検証を行うことを特徴とするものである。
【００２３】
また、本発明は、複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証を行うプログラムの検証装置であって、前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出部と、前記検出部により検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成するモデル生成部と、前記モデル生成部により生成された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証部とを備えたものである。
【００２４】
また、本発明に係るプログラムの検証装置において、前記検出部は、変更の影響を受ける共有変数が出現する部分と該共有変数のロックの部分を前記第１の部分とすることを特徴とするものである。
【００２５】
また、本発明に係るプログラムの検証装置において、前記検出部は、前記検証対象プログラムにおいて前記第１の部分にマークを付加し、前記モデル生成部は、前記マークを検出することにより前記第１の部分と前記第２の部分への分類を行うことを特徴とするものである。
【００２６】
また、本発明に係るプログラムの検証装置において、前記モデル生成部は、前記第１の部分と前記第２の部分の基本ブロックを状態に割り付け、前記制御構造部分に基づいて遷移を表すことにより、有限状態機械をモデルとして生成することを特徴とするものである。
【００２７】
また、本発明に係るプログラムの検証装置において、前記モデル生成部は、前記モデルにおいて、前記第１の部分を含まない複数の状態をまとめて１つの状態とすることを特徴とするものである。
【００２８】
また、本発明に係るプログラムの検証装置において、前記検証部は、まず、前記変更が施された関数について変更前のモデルと変更後のモデルの比較を行い、該比較の結果が一致しない場合、前記変更が施された関数のモデルと前記変更の影響を受ける共有変数を用いた関数のモデルの状態の積で得られるモデルについて、変更前のモデルと変更後のモデルの比較を行うことにより、前記変更後の検証対象プログラムの検証を行うことを特徴とするものである。
【００２９】
また、本発明に係るプログラムの検証装置において、前記検証部は、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態を表示することを特徴とするものである。
【００３０】
また、本発明に係るプログラムの検証装置において、前記検証部は、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態に至る実行順序を検出し、該実行順序を表示することを特徴とするものである。
【００３１】
また、本発明に係るプログラムの検証装置において、前記検証部は、ルールベースチェックまたはモデルチェックを用いて、変更後の検証対象プログラムの検証を行うことを特徴とするものである。
【００３２】
また、本発明は、並行プログラムまたは並列プログラムを検証対象プログラムとし、変更が施された検証対象プログラムの検証を行うプログラムの検証方法であって、前記変更前の検証対象プログラムと前記変更後の検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数を用いた関数とを検出すると共に、検出した関数から前記変更の影響を受ける部分である第１の部分を検出する検出ステップと、前記検出ステップにより検出された各関数から、制御構造、第１の部分、前記制御構造と前記第１の部分以外の部分である第２の部分に分類し、該分類に基づいて前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成するモデル生成ステップと、前記モデル生成ステップにより生成された、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証ステップとを実行するものである。
【発明の効果】
【００３３】
本発明によれば、並行・並列プログラムの検証に要する時間を大幅に短縮することにより、対話的デバッグ作業が可能になり、並行・並列プログラムの開発効率を大幅に向上させることができる。
【発明を実施するための最良の形態】
【００３４】
以下、本発明の実施の形態について図面を参照しつつ説明する。
【００３５】
実施の形態１．
本実施の形態では、同期機構としてＭＵＴＥＸロックを用い、プログラムの変更により、データ競合が起こる場合について説明する。
【００３６】
図１は、本発明に係るプログラムの検証装置の構成の一例を示すブロック図である。この検証装置は、変更検出部１１、ソースコード分類部１２、モデル生成部１３、検証部１４を備える。
【００３７】
ここで、検証装置の動作の説明のために、並列プログラムの具体例である第１の検証対象プログラムを用いて説明する。この第１の検証対象プログラムのソースコードは、共有変数の定義、関数Ｐｒｏｃｅｓｓ１、関数Ｐｒｏｃｅｓｓ２から成る。図２は、第１の検証対象プログラムにおける共有変数の定義を示すソースコードである。また、図３は、第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１を示すソースコードである。また、図４は、第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２を示すソースコードである。また、図５は、第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１を示すソースコードである。このように関数Ｐｒｏｃｅｓｓ１を変更した場合、関数Ｐｒｏｃｅｓｓ１と関数Ｐｒｏｃｅｓｓ２の間で共有変数ｓｈａｒｅｄ１に対するデータ競合が起こる。
【００３８】
図６は、本発明に係るプログラムの検証装置の動作の一例を示すフローチャートである。
【００３９】
まず、変更検出部１１は、変更前プログラムと変更後プログラムを読み込んで、それらの差分を確認する変更検出処理を行う（Ｓ１１）。
【００４０】
図７は、本発明に係る変更検出処理の動作の一例を示すフローチャートである。まず、変更検出部１１は、変更前プログラムと変更後プログラムを比較し、変更された関数Ｊ、変更に影響を受けた共有変数集合Ｖを特定する（Ｓ２１）。次に、変更検出部１１は、変更後の関数Ｊにおいて共有変数集合Ｖの出現する部分とロックの部分にマークを付加する（Ｓ２２）。次に、変更検出部１１は、変更前の関数Ｊにおいて共有変数集合Ｖの出現する部分とロックの部分にマークを付加する（Ｓ２３）。次に、変更検出部１１は、他の関数の中から共有変数集合Ｖが出現する関数Ｋを特定する（Ｓ２４）。次に、変更検出部１１は、関数Ｋにおいて共有変数集合Ｖの出現する部分とロックの部分にマークを付加する（Ｓ２５）。次に、変更検出部１１は、マークが付いた関数集合を出力し（Ｓ２６）、このフローを終了する。
【００４１】
ここで、変更検出処理の具体例について説明する。図８は、第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１の変更検出処理の結果の一例を示すソースコードである。ここで、まず、変更検出部１１は、変更された関数が関数Ｐｒｏｃｅｓｓ１のみであると特定し、関数Ｐｒｏｃｅｓｓ１の変更箇所を特定し、特定した箇所に“／／１”から“／／６”までのマークを付加する。次に、変更検出部１１は、変更箇所で用いられている共有変数がｓｈａｒｅｄ１であると特定する。
【００４２】
図９は、第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１の変更検出処理の結果の一例を示すソースコードである。次に、変更前のＰｒｏｃｅｓｓ１におけるｓｈａｒｅｄ１の出現箇所を特定し、特定した箇所に“／／Ｓ”のマークを付加する。図１０は、第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２の変更検出処理の結果の一例を示すソースコードである。次に、変更検出部１１は、変数ｓｈａｒｅｄ１を使う別のプロセスを検索し、関数Ｐｒｏｃｅｓｓ２を特定し、関数Ｐｒｏｃｅｓｓ１におけるｓｈａｒｅｄ１の出現箇所を特定し、特定した箇所に“／／Ｓ”のマークを付加する。この結果、変更検出部１１の出力は、変更前の関数Ｐｒｏｃｅｓｓ１、変更後の関数Ｐｒｏｃｅｓｓ１、関数Ｐｒｏｃｅｓｓ２の関数集合であり、変更が施された部分や変更に影響を受けた部分にマークが付加されたソースコードである。
【００４３】
次に、ソースコード分類部１２は、制御構造、変更の影響を受ける部分、それ以外の部分の分類を行う（Ｓ１２）。ソースコード分類部１２は、対象となる関数において、制御構造とマークが付いている文を残した上で、基本ブロック単位で文をまとめる。基本ブロックとは、コンパイラ技術に使われる定義であり、制御フローの入口と出口がそれぞれ１つしかないブロックを指す。
【００４４】
図１１は、本発明に係るソースコード分類処理の動作の一例を示すフローチャートである。まず、ソースコード分類部１２は、変更検出部１１の出力である関数集合からある関数ｊを取り出す（Ｓ３１）。次に、ソースコード分類部１２は、関数ｊから制御構造を抽出し、新しい抽出関数ｊ’に出力する（Ｓ３２）。次に、ソースコード分類部１２は、関数ｊからマークが付いている部分を抽出し、抽出関数ｊ’に出力する（Ｓ３３）。次に、ソースコード分類部１２は、関数ｊからマークが付いていない部分を基本ブロック単位にまとめて抽出し、抽出関数ｊ’に出力する（Ｓ３４）。次に、ソースコード分類部１２は、関数集合に未処理の関数が残っているか否かの判断を行う（Ｓ３５）。関数が残っている場合（Ｓ３５，Ｙ）、処理Ｓ３１へ戻る。一方、関数が残っていない場合（Ｓ３５，Ｎ）、抽出関数ｊ’の集合を抽出関数集合として出力し（Ｓ３６）、このフローを終了する。
【００４５】
ここで、ソースコード分類処理の具体例について説明する。図１２は、第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１のソースコード分類処理の結果の一例を示すソースコードである。変更前の関数Ｐｒｏｃｅｓｓ１の基本ブロックは、擬似関数ＡＡ（）、擬似関数ＢＢ（）、擬似関数ＣＣ（）、擬似関数ＤＤ（）、擬似関数ＥＥ（）としてまとめられる。図１３は、第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２のソースコード分類処理の結果の一例を示すソースコードである。関数Ｐｒｏｃｅｓｓ２の基本ブロックは、擬似関数ＸＸ（）、擬似関数ＺＺ（）としてまとめられる。
【００４６】
図１４は、第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１のソースコード分類処理の結果の一例を示すソースコードである。ここで、変更後の関数Ｐｒｏｃｅｓｓ１の基本ブロックは、関数ａ（）と関数ｂ（）を擬似関数Ａ（）、関数ｄ（）を擬似関数Ｂ（）、関数ｅ（）を擬似関数Ｃ（）、関数ｌ．ｌｏｃｋ（）から関数ｆ（）までを擬似関数Ｄ（）、関数ｈ（）を擬似関数Ｅ（）としてまとめられる。
【００４７】
次に、モデル生成部１３は、ソースコード分類処理の結果をモデルに変換する（Ｓ１３）。モデルの種類は、後述する検証処理で用いる技術により異なるが、本実施の形態では、検証処理にモデルチェックを用い、モデルとしてＦＳＭを用いる。モデル生成部１３は、ソースコード分類処理の結果のうち、基本ブロック単位または共有変数を参照するブロック単位で状態を割り付け、更に状態最適化を行う。状態最適化は、マークが付いた部分が含まれない状態を１つの状態にまとめるものであり、State Minimizationアルゴリズムの応用により実現可能である。
【００４８】
図１５は、本発明に係るモデル生成処理の動作の一例を示すフローチャートである。まず、モデル生成部１３は、ソースコード分類部１２の出力である抽出関数集合からある抽出関数ｊ’を取り出す（Ｓ４１）。次に、モデル生成部１３は、ロックで保護されている部分を基本ブロックと見なす（Ｓ４２）。次に、モデル生成部１３は、抽出関数ｊ’の制御構造を辿り、基本ブロックを１つ取り出す（Ｓ４３）。次に、モデル生成部１３は、基本ブロック内にマークが付いた部分が存在するか否かの判断を行う（Ｓ４４）。マークが付いた部分が存在する場合（Ｓ４４，Ｙ）、モデル生成部１３は、基本ブロックからマークが付いた部分を分離し、１つの状態に割り付け（Ｓ４５）、残った部分をそれぞれ１つの状態に割り付け（Ｓ４６）、処理Ｓ４８へ移行する。一方、マークが付いた部分が存在しない場合（Ｓ４４，Ｎ）、モデル生成部１３は、基本ブロックを１つの状態に割り付け（Ｓ４７）、処理Ｓ４８へ移行する。
【００４９】
次に、処理Ｓ４８において、モデル生成部１３は、未処理の基本ブロックが残っているか否かの判断を行う（Ｓ４８）。未処理の基本ブロックが残っている場合（Ｓ４８，Ｙ）、処理Ｓ４３へ戻る。一方、未処理の基本ブロックが残っていない場合（Ｓ４８，Ｎ）、モデル生成部１３は、状態最適化を行う（Ｓ４９）。次に、モデル生成部１３は、抽出関数集合に未処理の抽出関数が残っているか否かの判断を行う（Ｓ５０）。未処理の抽出関数が残っている場合（Ｓ５０，Ｙ）、処理Ｓ４１へ戻る。一方、未処理の抽出関数が残っていない場合（Ｓ５０，Ｎ）、モデル生成部１３は、状態最適化の結果をＦＳＭモデル集合として出力し（Ｓ５１）、このフローを終了する。
【００５０】
ここで、モデル生成処理の具体例について説明する。まず、処理Ｓ４８までの状態割り付けの結果について説明する。図１６は、第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の状態割り付けの結果の一例を示すモデルである。ここで、モデル生成部１３は、擬似関数Ａ（），関数ｃ（）を状態Ａ、擬似関数Ｂ（）を状態Ｂ、擬似関数Ｃ（）を状態Ｃ、擬似関数Ｄ（）を状態Ｄ、擬似関数Ｅ（）を状態Ｅ、“／／１”，“／／２”，“／／３”を状態Ｎ１２３、“／／４”，“／／５”，“／／６”を状態Ｎ４５６として、それぞれ割り付ける。次に、処理Ｓ４９の状態最適化の結果について説明する。図１７は、第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の結果の一例を示すモデルである。ここで、状態Ａ、状態Ｂ，状態Ｃ，状態Ｄは、１つの基本ブロックとなり、かつ、その中にマークが付いた部分が存在しないため、状態Ａ’に統合される。
【００５１】
同様に、モデル生成部１３は、変更前の関数Ｐｒｏｃｅｓｓ１と関数Ｐｒｏｃｅｓｓ２に対してモデル生成処理を行う。図１８は、第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の状態割り付けの結果の一例を示すモデルである。擬似関数ＡＡ（）、擬似関数ＢＢ（）、擬似関数ＣＣ（）、擬似関数ＤＤ（）、擬似関数ＥＥ（）は、それぞれ状態ＡＡ、状態ＢＢ、状態ＣＣ、状態ＤＤ、状態ＥＥに割り付けられ、マーク“／／Ｓ”の付いた部分は状態Ｎ１に割り付けられる。図１９は、第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の結果の一例を示すモデルである。状態ＡＡ、状態ＢＢ、状態ＣＣ、状態ＤＤは、１つの基本ブロックとなり、かつ、その中にマークが付いた部分が存在しないため、状態ＡＡ’に統合される。
【００５２】
図２０は、第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２のモデル生成処理の結果の一例を示すモデルである。擬似関数ＸＸ（）、擬似関数ＺＺ（）は、それぞれ状態ＸＸ、状態ＺＺに割り付けられ、マーク“／／Ｓ”の付いた部分は状態Ｎ２に割り付けられる。状態最適化による変化はない。
【００５３】
次に、検証部１４は、モデル生成処理の結果を用いて検証処理を行う（Ｓ１４）。検証処理の方法として、モデルチェック、ルールベースチェック等があるが、本実施の形態では、検証処理にモデルチェックを用いる。
【００５４】
図２１は、本発明に係る検証処理の動作の一例を示すフローチャートである。まず、検証部１４は、モデル生成部１３の出力であるＦＳＭモデル集合のうち変更された関数に対してモデルチェックを行い（Ｓ６１）、モデルが一致したか否かの判断を行う（Ｓ６２）。モデルが一致した場合（Ｓ６２，Ｙ）、処理Ｓ６８へ移行する。一方、モデルが一致しない場合（Ｓ６２，Ｎ）、検証部１４は、検証する関数の範囲を拡大し、モデルチェックを行い（Ｓ６３）、モデルが一致したか否かの判断を行う（Ｓ６４）。モデルが一致した場合（Ｓ６４，Ｙ）、処理Ｓ６８へ移行する。一方、モデルが一致しない場合（Ｓ６４，Ｎ）、検証部１４は、問題箇所を表示し（Ｓ６６）、可能であればプログラムの動作に対する制約を付加し、必要があれば設計者の指示に従ってａｓｓｅｒｔｉｏｎの挿入を行い（Ｓ６７）、処理Ｓ６３へ戻る。また、処理Ｓ６８において、検証部１４は、変更による問題がないことを表示し（Ｓ６８）、このフローを終了する。
【００５５】
検証処理においてはまず、変更が施された関数について変更前のモデルと変更後のモデルの比較を行い、モデルチェックを行う。検証処理の結果、モデルが一致した場合、変更された箇所は変更前と同じ振る舞いをする保証があることから、プログラム全体として不具合は起こらないと保証できる。また、モデルが一致しない場合、不具合が起こる可能性があり、検証する関数の範囲を広げ、変更された関数以外に変更検出処理で検出された関数を含めて検証を行う。その結果、不具合が発見されなければ、プログラム全体として不具合は起きないと保証できる。
【００５６】
ここで、検証の範囲を広げ、並行・並列に動作する複数の関数の相互影響を表すためには、各関数のモデルの半順序関係を考慮して状態の積を作成する。この状態の積に対して範囲を広げた検証を行う。状態の積を求めるアルゴリズムは従来に定義されているものを使う。例えば、Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P. "Systems and Software Verification Model-Checking Techniques and Tools", Springer-Verlag, 2001 にアルゴリズムの詳しい説明が掲載されている。
【００５７】
また、検証処理により問題点が発見された場合、処理Ｓ６６において不具合が起こる原因を示すために、例えば実行順序を出力するトレース生成処理が有効な手段である。図２２は、本発明に係るトレース生成処理の動作の一例を示すフローチャートである。トレース生成処理における入力は、ＦＳＭと検証するプロパティである。本実施の形態において、検証するプロパティは、デッドロックまたはデータ競合が存在するか否かの確認である。まず、検証部１４は、ＦＳＭにおいて検証するプロパティを満足する状態を、初期状態から順に探索し（Ｓ７１）、検証するプロパティを満足する状態が存在するか否かの判断を行う（Ｓ７２）。検証するプロパティを満足する状態が存在しない場合（Ｓ７２，Ｎ）、検証部１４は、モデルにデッドロックやデータ競合は起きないと判断し（Ｓ７３）、このフローを終了する。一方、検証するプロパティを満足する状態が存在する場合（Ｓ７２，Ｙ）、検証部１４は、初期状態から検証するプロパティを満足する状態までの実行順序をトレースとして出力し（Ｓ７５）、このフローを終了する。
【００５８】
また、再度、広範囲の検証を行う場合、処理Ｓ６３において設計者はプログラムの動作上の制約を設定してから検証を行うことができる。ここで、設計者がソースコードにａｓｓｅｒｔｉｏｎとして入力することにより、デバッグ終了後、テストを行うときに制約が守られていない場合、その箇所の検出が容易となる。
【００５９】
ここで、検証処理の具体例について説明する。この例では、まず、変更前と変更後の関数Ｐｒｏｃｅｓｓ１のモデルを比較する。結果はモデルと一致しないことから、不具合が起こる可能性があり、関数Ｐｒｏｃｅｓｓ１の変更によって影響を受ける可能性のある関数Ｐｒｏｃｅｓｓ２を含めて再度検証処理を行う。その結果、不具合が起こることが検出されると共に、次の実行順序で不具合が起こることが検出され、検証部１４により表示される。
【００６０】
ＸＸ→Ａ’→Ｎ１２３→Ｅ→Ｎ２→Ｎ４５６→ＺＺ
【００６１】
変更前の関数Ｐｒｏｃｅｓｓ１において、変数ｓｈａｒｅｄ１の読み出し（関数ｇの呼び出し）と書き込みは、ロックに保護されているので関数Ｐｒｏｃｅｓｓ２に割り込まれることはない。また、関数Ｐｒｏｃｅｓｓ２においてロックによる保護が実行されるとき、共有変数ｓｈａｒｅｄ１は、必ず関数Ｐｒｏｃｅｓｓ１の関数ｇが呼ばれた後に値がインクリメントされたものになっている。
【００６２】
一方、変更後の関数Ｐｒｏｃｅｓｓ１を用いる不具合の実行順序の場合、状態Ｎ１２３（関数ｇの呼び出し）と状態Ｎ４５６（変数ｓｈａｒｅｄ１の書き込み）は、それぞれロックに保護されており、その間に関数Ｐｒｏｃｅｓｓ２の状態Ｎ２（ロックに保護されている領域）が実行される。状態Ｎ２が実行されるとき、変数ｓｈａｒｅｄ１の値はインクリメントされていない。従って、変更前の挙動と異なり、不具合が起こる。
【００６３】
上記の不具合に対して、設計者が制約を設けて不具合を解消できることが可能である。このプログラムの場合は、例えば関数Ｐｒｏｃｅｓｓ１が状態Ｎ１２３、状態Ｅ、状態Ｎ４５６にいる間は、関数Ｐｒｏｃｅｓｓ２の状態Ｎ２の割り込みを禁止すれば、不具合は起こらない。
【００６４】
実施の形態２．
本実施の形態では、共有変数へのアクセスを調停する同期機構の順番が変わってデッドロックが起こる場合について説明する。
【００６５】
検証装置の構成は実施の形態１と同様である。また、検証装置の動作の説明のために、並列プログラムの具体例である第２の検証対象プログラムを用いて説明する。この第２の検証対象プログラムのソースコードは、共有変数の定義、関数Ｐｒｏｃｅｓｓ３、関数Ｐｒｏｃｅｓｓ４から成る。図２３は、第２の検証対象プログラムにおける共有変数の定義を示すソースコードである。また、図２４は、第２の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ３を示すソースコードである。また、図２５は、第２の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ４を示すソースコードである。
【００６６】
図２６は、第２の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ４を示すソースコードである。図に示すように関数Ｐｒｏｃｅｓｓ４は、ロックの順序を変更した。この変更により、関数Ｐｒｏｃｅｓｓ３と関数Ｐｒｏｃｅｓｓ４が共有変数をアクセスする際にロックをかける順序は、それぞれ異なる。
【００６７】
図２７は、第２の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ４のソースコード分類処理の結果の一例を示すソースコードである。次に、モデル生成処理により、擬似関数Ｄ（）は状態Ｄに、擬似関数Ｆ（）は状態Ｆに割り付けられる。ここでは、ロックに保護されている領域（“／／Ｅ”のマークが付いた領域）は、基本ブロックと見なされ、状態展開処理が実行される。つまり、本実施の形態においては、モデル生成処理における処理Ｓ４５の代わりに次に述べる状態展開処理を行う。
【００６８】
図２８は、本発明に係る状態展開処理の動作の一例を示すフローチャートである。まず、モデル生成部１３は、処理Ｓ４５によりマークが付いて分離された基本ブロックの一部において、複数のロックが存在するか否かの判断を行う（Ｓ８１）。複数のロックが存在しない場合（Ｓ８１，Ｎ）、処理Ｓ４５と同様、モデル生成部１３は、マークが付いた状態を１つの状態に割り付け（Ｓ８２）、変更したＦＳＭモデルを出力し（Ｓ８３）、このフローを終了する。一方、複数のロックが存在する場合（Ｓ８１，Ｙ）、モデル生成部１３は、各ロックが取り得る状態をＦＳＭの状態に割り付け（Ｓ８５）、ロックに保護されている演算を１つの状態に割り付け（Ｓ８６）、ロックと演算の状態遷移を元の基本ブロックの制御フローに合わせ（Ｓ８７）、変更したＦＳＭモデルを出力し（Ｓ８８）、このフローを終了する。
【００６９】
処理Ｓ８３では、ロックが取り得る状態にＦＳＭの状態を割り付ける。その結果、次の４つの状態が割り付けられる。
【００７０】
状態Ｎ１０．演算する前にロックｍの獲得
状態Ｎ２０．演算する前、かつロックｍの獲得の後、ロックｌの獲得
状態Ｎ３０．演算した直後、ロックｌの解放
状態Ｎ４０．演算した後、かつロックｌの解放の後、ロックｍの解放
【００７１】
処理Ｓ８４では、演算を１つの状態に割り付ける。この場合、上記の状態Ｎ２０と状態Ｎ３０の間に１つの状態が割り付けられ、次の５つの状態になる。
【００７２】
状態Ｎ１０．演算する前にロックｍの獲得
状態Ｎ２０．演算する前、かつロックｍの獲得の後、ロックｌの獲得
状態Ｎ２５．演算
状態Ｎ３０．演算した直後、ロックｌの解放
状態Ｎ４０．演算した後、かつロックｌの解放の後、ロックｍの解放
【００７３】
図２９は、第２の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ４のモデル生成処理の結果の一例を示す状態遷移図である。ここで、状態Ｌ（Ｕ）はロックｌがアンロックである状態、状態Ｌ（３）は関数Ｐｒｏｃｅｓｓ３がロックｌを獲得した状態、状態Ｌ（４）は関数Ｐｒｏｃｅｓｓ４がロックｌを獲得した状態、状態Ｍ（Ｕ）はロックｍがアンロックである状態、状態Ｍ（３）は関数Ｐｒｏｃｅｓｓ３がロックｍを獲得した状態、状態Ｍ（４）は関数Ｐｒｏｃｅｓｓ４がロックｍを獲得した状態をそれぞれ表し、更に複数の関数を検証の対象とする場合は、各状態の積で表す。この図の状態Ｌ（Ｕ）Ｍ（４）から状態Ｌ（Ｕ）Ｍ（Ｕ）は、状態Ｎ１０から状態Ｎ４０に相当する。関数Ｐｒｏｃｅｓｓ３と変更前の関数Ｐｒｏｃｅｓｓ４のＦＳＭも、同様の手順で得られる。図３０は、第２の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ３のモデル生成処理の結果の一例を示す状態遷移図である。図３１は、第２の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ４のモデル生成処理の結果の一例を示す状態遷移図である。
【００７４】
次に、検証処理の処理Ｓ６１において、変更前と変更後の関数Ｐｒｏｃｅｓｓ４を比較すると一致しない。そこで、検証する関数の範囲を広げて関数Ｐｒｏｃｅｓｓ３を含めた検証を行う。並行に動作する関数Ｐｒｏｃｅｓｓ３と関数Ｐｒｏｃｅｓｓ４の影響を合わせて検証するためには、半順序関係を考慮して両関数の状態の積を作成し、その状態の積を検証する。このモデルチェックにより、以下の実行順序がデッドロックへと導くことが分かる。
【００７５】
Ａ→Ｄ→Ｌ（３）Ｍ（Ｕ）→Ｌ（３）Ｍ（４）→デッドロック
【００７６】
デッドロックの原因は、関数Ｐｒｏｃｅｓｓ３がロックｌを獲得した後（状態Ｌ（３）Ｍ（Ｕ））、関数Ｐｒｏｃｅｓｓ４がロックｍを獲得した（状態Ｌ（３）Ｍ（４））ためである。このとき、ロックｌとロックｍはそれぞれ関数Ｐｒｏｃｅｓｓ３と関数Ｐｒｏｃｅｓｓ４に獲得されている。仮に関数Ｐｒｏｃｅｓｓ３がロックｍの獲得を試みた場合、関数Ｐｒｏｃｅｓｓ４が既に獲得しているので処理は止まってしまう。同様に、関数Ｐｒｏｃｅｓｓ４がロックｌの獲得を試みた場合、関数Ｐｒｏｃｅｓｓ３が既に獲得しているので処理は止まってしまう。また、この例の場合、不具合を修正するためには変更を元に戻すしかない。
【００７７】
以上詳述したように、本発明によれば、並行・並列プログラムの変更に影響を受ける共有リソースとロックに着目したモデルを作成することにより、検証に要する時間を大幅に短縮することができる。
【００７８】
更に、プログラムの検証装置を構成するコンピュータにおいて上述した各ステップを実行させるプログラムを、プログラムの検証プログラムとして提供することができる。上述したプログラムは、コンピュータにより読取り可能な記録媒体に記憶させることによって、プログラムの検証装置を構成するコンピュータに実行させることが可能となる。ここで、上記コンピュータにより読取り可能な記録媒体としては、ＲＯＭやＲＡＭ等のコンピュータに内部実装される内部記憶装置、ＣＤ−ＲＯＭやフレキシブルディスク、ＤＶＤディスク、光磁気ディスク、ＩＣカード等の可搬型記憶媒体や、コンピュータプログラムを保持するデータベース、或いは、他のコンピュータ並びにそのデータベースや、更に回線上の伝送媒体をも含むものである。
【００７９】
なお、検出ステップとは、実施の形態における変更検出処理とソースコード分類処理に対応する。また、モデル生成ステップとは、実施の形態におけるとモデル生成処理に対応する。また、検証ステップとは、実施の形態における検証処理に対応する。また、検出部とは、実施の形態における変更検出部とソースコード分類部に対応する。
【００８０】
（付記１）  複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証をコンピュータに実行させるプログラムの検証プログラムであって、
前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出ステップと、
前記検出ステップにより検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成するモデル生成ステップと、
前記モデル生成ステップにより生成された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証ステップと、
をコンピュータに実行させるプログラムの検証プログラム。
（付記２）  付記１に記載のプログラムの検証プログラムにおいて、
前記検出ステップは、前記変更の影響を受ける共有変数が出現する部分と該共有変数のロックの部分を前記第１の部分とすることを特徴とするプログラムの検証プログラム。
（付記３）  付記１または付記２に記載のプログラムの検証プログラムにおいて、
前記検出ステップは、前記検証対象プログラムにおいて前記第１の部分にマークを付加することを特徴とするプログラムの検証プログラム。
（付記４）  付記１乃至付記３のいずれかに記載のプログラムの検証プログラムにおいて、
前記モデル生成ステップは、前記第１の部分と前記第２の部分の基本ブロックを状態に割り付け、前記制御構造部分に基づいて遷移を表すことにより、有限状態機械をモデルとして生成することを特徴とするプログラムの検証プログラム。
（付記５）  付記４に記載のプログラムの検証プログラムにおいて、
前記モデル生成ステップは、前記モデルにおいて、前記第１の部分を含まない複数の状態をまとめて１つの状態とすることを特徴とするプログラムの検証プログラム。
（付記６）  付記４または付記５に記載のプログラムの検証プログラムにおいて、
前記検証ステップは、まず、前記変更が施された関数について変更前のモデルと変更後のモデルの比較を行い、該比較の結果が一致しない場合、前記変更が施された関数のモデルと前記変更の影響を受ける共有変数を用いた関数のモデルの状態の積で得られるモデルについて、変更前のモデルと変更後のモデルの比較を行うことにより、前記変更後の検証対象プログラムの検証を行うことを特徴とするプログラムの検証プログラム。
（付記７）  付記１乃至付記６のいずれかに記載のプログラムの検証プログラムにおいて、
前記検証ステップは、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態を表示することを特徴とするプログラムの検証プログラム。
（付記８）  付記１乃至付記７のいずれかに記載のプログラムの検証プログラムにおいて、
前記検証ステップは、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態に至る実行順序を検出し、該実行順序を表示することを特徴とするプログラムの検証プログラム。
（付記９）  付記１乃至付記８のいずれかに記載のプログラムの検証プログラムにおいて、
前記検証ステップは、ルールベースチェックまたはモデルチェックを用いて、変更後の検証対象プログラムの検証を行うことを特徴とするプログラムの検証プログラム。
（付記１０）  複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証を行うプログラムの検証装置であって、
前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出部と、
前記検出部により検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成するモデル生成部と、
前記モデル生成部により生成された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証部と、
を備えてなるプログラムの検証装置。
（付記１１）  付記１０に記載のプログラムの検証装置において、
前記検出部は、前記変更の影響を受ける共有変数が出現する部分と該共有変数のロックの部分を前記第１の部分とすることを特徴とするプログラムの検証装置。
（付記１２）  付記１０または付記１１に記載のプログラムの検証装置において、
前記検出部は、前記検証対象プログラムにおいて前記第１の部分にマークを付加することを特徴とするプログラムの検証装置。
（付記１３）  付記１０乃至付記１２のいずれかに記載のプログラムの検証装置において、
前記モデル生成部は、前記第１の部分と前記第２の部分の基本ブロックを状態に割り付け、前記制御構造部分に基づいて遷移を表すことにより、有限状態機械をモデルとして生成することを特徴とするプログラムの検証装置。
（付記１４）  付記１３に記載のプログラムの検証装置において、
前記モデル生成部は、前記モデルにおいて、前記第１の部分を含まない複数の状態をまとめて１つの状態とすることを特徴とするプログラムの検証装置。
（付記１５）  付記１３または付記１４に記載のプログラムの検証装置において、
前記検証部は、まず、前記変更が施された関数について変更前のモデルと変更後のモデルの比較を行い、該比較の結果が一致しない場合、前記変更が施された関数のモデルと前記変更の影響を受ける共有変数を用いた関数のモデルの状態の積で得られるモデルについて、変更前のモデルと変更後のモデルの比較を行うことにより、前記変更後の検証対象プログラムの検証を行うことを特徴とするプログラムの検証装置。
（付記１６）  付記１０乃至付記１５のいずれかに記載のプログラムの検証装置において、
前記検証部は、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態を表示することを特徴とするプログラムの検証装置。
（付記１７）  付記１０乃至付記１６のいずれかに記載のプログラムの検証装置において、
前記検証部は、変更前の検証対象プログラムのモデルと変更後の検証対象プログラムのモデルが一致しない場合、所定の不具合となる状態を検出し、該状態に至る実行順序を検出し、該実行順序を表示することを特徴とするプログラムの検証装置。
（付記１８）  付記１０乃至付記１７のいずれかに記載のプログラムの検証装置において、
前記検証部は、ルールベースチェックまたはモデルチェックを用いて、変更後の検証対象プログラムの検証を行うことを特徴とするプログラムの検証装置。
（付記１９）  複数の関数を含んで構成される並行プログラムまたは並列プログラムを検証対象プログラムとし、該検証対象プログラムを変更した場合における該変更後の検証対象プログラムの検証を行うプログラムの検証方法であって、
前記検証対象プログラムの変更前後における該検証対象プログラムから、前記変更が施された関数と、前記変更の影響を受ける共有変数が用いられる関数とを検出すると共に、前記変更が施された関数における前記変更が施された部分及び前記変更の影響を受ける共有変数を用いた関数における変更の影響を受ける部分である第１の部分と、プログラム処理の制御に関する部分である制御構造部分と、前記制御構造部分と前記第１の部分以外の部分である第２の部分を検出する検出ステップと、
前記検出ステップにより検出された前記制御構造部分と前記第１の部分と前記第２の部分に基づいて、前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを生成するモデル生成ステップと、
前記モデル生成ステップにより生成された前記変更前の検証対象プログラムのモデルと前記変更後の検証対象プログラムのモデルを比較することにより、前記変更後の検証対象プログラムの検証を行う検証ステップと、
を実行するプログラムの検証方法。
（付記２０）  付記１９に記載のプログラムの検証方法において、
前記検出ステップは、前記変更の影響を受ける共有変数が出現する部分と該共有変数のロックの部分を前記第１の部分とすることを特徴とするプログラムの検証方法。
【図面の簡単な説明】
【００８１】
【図１】本発明に係るプログラムの検証装置の構成の一例を示すブロック図である。
【図２】第１の検証対象プログラムにおける共有変数の定義を示すソースコードである。
【図３】第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１を示すソースコードである。
【図４】第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２を示すソースコードである。
【図５】第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１を示すソースコードである。
【図６】本発明に係るプログラムの検証装置の動作の一例を示すフローチャートである。
【図７】本発明に係る変更検出処理の動作の一例を示すフローチャートである。
【図８】第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１の変更検出処理の結果の一例を示すソースコードである。
【図９】第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１の変更検出処理の結果の一例を示すソースコードである。
【図１０】第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２の変更検出処理の結果の一例を示すソースコードである。
【図１１】本発明に係るソースコード分類処理の動作の一例を示すフローチャートである。
【図１２】第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１のソースコード分類処理の結果の一例を示すソースコードである。
【図１３】第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２のソースコード分類処理の結果の一例を示すソースコードである。
【図１４】第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１のソースコード分類処理の結果の一例を示すソースコードである。
【図１５】本発明に係るモデル生成処理の動作の一例を示すフローチャートである。
【図１６】第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の状態割り付けの結果の一例を示すモデルである。
【図１７】第１の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の結果の一例を示すモデルである。
【図１８】第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の状態割り付けの結果の一例を示すモデルである。
【図１９】第１の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ１のモデル生成処理の結果の一例を示すモデルである。
【図２０】第１の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ２のモデル生成処理の結果の一例を示すモデルである。
【図２１】本発明に係る検証処理の動作の一例を示すフローチャートである。
【図２２】本発明に係るトレース生成処理の動作の一例を示すフローチャートである。
【図２３】第２の検証対象プログラムにおける共有変数の定義を示すソースコードである。
【図２４】第２の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ３を示すソースコードである。
【図２５】第２の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ４を示すソースコードである。
【図２６】第２の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ４を示すソースコードである。
【図２７】第２の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ４のソースコード分類処理の結果の一例を示すソースコードである。
【図２８】本発明に係る状態展開処理の動作の一例を示すフローチャートである。
【図２９】第２の検証対象プログラムにおける変更後の関数Ｐｒｏｃｅｓｓ４のモデル生成処理の結果の一例を示す状態遷移図である。
【図３０】第２の検証対象プログラムにおける関数Ｐｒｏｃｅｓｓ３のモデル生成処理の結果の一例を示す状態遷移図である。
【図３１】第２の検証対象プログラムにおける変更前の関数Ｐｒｏｃｅｓｓ４のモデル生成処理の結果の一例を示す状態遷移図である。
【図３２】並列プログラムにおける共有変数の定義の一例を示すソースコードである。
【図３３】並列プログラムにおける関数Ｐｒｏｃｅｓｓ０１の一例を示すソースコードである。
【図３４】並列プログラムにおける関数Ｐｒｏｃｅｓｓ０２の一例を示すソースコードである。
【図３５】並列プログラムにおける関数Ｐｒｏｃｅｓｓ０１の修正結果の一例を示すソースコードである。
【図３６】並列プログラムにおける関数Ｐｒｏｃｅｓｓ０２の修正結果の一例を示すソースコードである。
【符号の説明】
【００８２】
１１  変更検出部、１２  ソースコード分類部、１３  モデル生成部、１４  検証部。
【図１】
0004414373.tif 000002
【図２】
0004414373.tif 000003
【図３】
0004414373.tif 000004
【図４】
0004414373.tif 000005
【図５】
0004414373.tif 000006
【図６】
0004414373.tif 000007
【図７】
0004414373.tif 000008
【図８】
0004414373.tif 000009
【図９】
0004414373.tif 000010
【図１０】
0004414373.tif 000011
【図１１】
0004414373.tif 000012
【図１２】
0004414373.tif 000013
【図１３】
0004414373.tif 000014
【図１４】
0004414373.tif 000015
【図１５】
0004414373.tif 000016
【図１６】
0004414373.tif 000017
【図１７】
0004414373.tif 000018
【図１８】
0004414373.tif 000019
【図１９】
0004414373.tif 000020
【図２０】
0004414373.tif 000021
【図２１】
0004414373.tif 000022
【図２２】
0004414373.tif 000023
【図２３】
0004414373.tif 000024
【図２４】
0004414373.tif 000025
【図２５】
0004414373.tif 000026
【図２６】
0004414373.tif 000027
【図２７】
0004414373.tif 000028
【図２８】
0004414373.tif 000029
【図２９】
0004414373.tif 000030
【図３０】
0004414373.tif 000031
【図３１】
0004414373.tif 000032
【図３２】
0004414373.tif 000033
【図３３】
0004414373.tif 000034
【図３４】
0004414373.tif 000035
【図３５】
0004414373.tif 000036
【図３６】
0004414373.tif 000037