(57)【要約】【課題】検証時間を短縮化できるプログラム検証装置を提供する。【解決手段】プログラム検証装置は、検証対象プログラムの処理内容を解析し、前記検証対象プログラムの言語仕様のうちの検証対象の仕様である検証対象仕様を満たすか否かを判定するための検証式を生成する検証式生成部３０３と、生成した検証式を含む検証コードを生成する検証コード生成部３０４と、検証コード生成部３０４が生成した少なくとも２つの検証コードについて、１つの検証コードに合成可能か否かを判定し、合成可能である場合には、１つの検証コードに合成する検証コード合成部３０５と、合成可能な少なくとも２つの検証コードについては、検証コード合成部３０５が合成した検証コードを用いて検証対象仕様を満たすか否かを判定する検証実行部３０７と、を備えている。【選択図】図２
2012238235.tif 000002
【特許請求の範囲】
【請求項１】
検証対象プログラムの処理内容を解析し、前記検証対象プログラムの言語仕様のうちの検証対象の仕様である検証対象仕様を満たすか否かを判定するための検証式を生成する検証式生成手段と、
前記生成した検証式を含む検証コードを生成する検証コード生成手段と、
前記検証コード生成手段が生成した少なくとも２つの検証コードについて、１つの検証コードに合成可能か否かを判定し、合成可能である場合には、１つの検証コードに合成する検証コード合成手段と、
前記合成可能な少なくとも２つの検証コードについては、前記検証コード合成手段が合成した検証コードを用いて検証対象仕様を満たすか否かを判定する検証実行手段と、
を備えていることを特徴とするプログラム検証装置。
【請求項２】
前記検証実行手段は、前記検証コード合成手段が合成した検証コード、及び、前記検証コード生成手段が生成し、前記検証コード合成手段が合成しなかった検証コードをそれぞれ実行して、各検証コードについて、対応する検証対象仕様を満たすか否かを判定する、
ことを特徴とする請求項１に記載のプログラム検証装置。
【請求項３】
前記検証式生成手段は、前記検証対象プログラムの処理内容を解析して、前記検証対象仕様に対応する処理部分を判定し、該判定した処理部分それぞれについて、該処理部分に対応する検証対象仕様の前記検証式および該処理部分に対応する関数を示すデータを含む検証データを生成し、
前記検証コード生成手段は、前記判定した処理部分それぞれについて前記検証コードを生成し、
前記検証コード合成手段は、前記検証コード生成手段が生成した少なくとも２つの検証コードについて、前記検証データに基づき対応する関数を判定し、同一の関数に対応する少なくとも２つの検証コードについて、１つの検証コードに合成可能か否かを判定する、
ことを特徴とする請求項１又は２に記載のプログラム検証装置。
【請求項４】
前記検証実行手段が実行した検証コードが対応する検証対象仕様を満たさない場合、前記実行した検証コードに対応する第１の関数に、前記第１の関数だけでは値が不定となる変数が存在するか否かを判定し、値が不定となる変数が存在する場合、前記第１の関数を呼び出す第２の関数を特定して、再度、前記検証対象プログラムの検証を、前記プログラム検証装置に実行させる制御手段を、備えており、
前記検証コード生成手段は、再度の前記検証対象プログラムの検証時、前記第２の関数を、前記第１の関数の前記検証対象仕様に対応する処理部分の検証コードを生成する際に参照する、
ことを特徴とする請求項３に記載のプログラム検証装置。
【請求項５】
前記検証コード合成手段は、前記検証コード生成手段が生成した少なくとも２つの検証コードで使用されている変数が包含関係にある場合、前記少なくとも２つの検証コードを合成可能と判定することを特徴とする請求項３又は４に記載のプログラム検証装置。
【請求項６】
前記検証コード合成手段は、前記少なくとも２つの検証コードで使用されている変数が同一であり、前記少なくとも２つの検証コードの前記検証式を除いた部分が同一である場合、前記少なくとも２つの検証コードの前記検証式を合成して１つの検証式にすることを特徴とする請求項５に記載のプログラム検証装置。
【請求項７】
前記検証コード合成手段は、前記少なくとも２つの検証コードの内の第１の検証コードで使用されている検証式及び変数を除いた部分が、もう一方の第２の検証コードで使用されている検証式及び変数を除いた部分を包含する場合、前記第２の検証コードで使用されている検証式を、前記第１の検証コードに挿入することにより検証コードの合成を行うことを特徴とする請求項５に記載のプログラム検証装置。
【請求項８】
請求項１から７のいずれか１項に記載のプログラム検証装置としてコンピュータを機能させるプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はモデル検証技術によるプログラム検証装置に関する。
【背景技術】
【０００２】
プログラムの振る舞いを自動的且つ網羅的に検証する為の方法として、モデル検証技術が利用されている。具体的には、検証対象であるプログラム（以後、検証対象プログラムと呼ぶ。）から検証式を生成し、検証式からＳＰＩＮやＳＭＶの様なモデル検証ツールに応じた言語で記述された検証コードを生成する。そして、この検証コードをプログラム検証装置において動作させて、検証式違反の有無を確認するというものである。
【０００３】
モデル検証においては、検証対象プログラムの規模によっては、その状態数の多さに起因して検証が実行できなくなる問題が生じ得る。このため、特許文献１では、検証対象プログラムを、プログラム検証装置が取り扱えるサイズに分割する構成を開示している。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開平７−３３４５６６号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、特許文献１に記載の方法においては、分割により検証実行回数が増加し検証時間が長くなってしまう。したがって、状態数が多くなることを防ぎつつ、検証時間を短縮化することが求められている。
【０００６】
本発明は、検証時間を短縮化できるプログラム検証装置及びプログラムを提供するものである。
【課題を解決するための手段】
【０００７】
本発明によるプログラム検証装置は、検証対象プログラムの処理内容を解析し、前記検証対象プログラムの言語仕様のうちの検証対象の仕様である検証対象仕様を満たすか否かを判定するための検証式を生成する検証式生成手段と、生成した検証式を含む検証コードを生成する検証コード生成手段と、検証コード生成手段が生成した少なくとも２つの検証コードについて、１つの検証コードに合成可能か否かを判定し、合成可能である場合には、１つの検証コードに合成する検証コード合成手段と、合成可能な少なくとも２つの検証コードについては、検証コード合成手段が合成した検証コードを用いて検証対象仕様を満たすか否かを判定する検証実行手段と、を備えていることを特徴とする。
【発明の効果】
【０００８】
検証式に対応する検証コードを生成し、合成可能であるものについては複数の検証コードを１つの検証コードに合成することで、プログラム検証に要する時間を短縮化することができる。
【図面の簡単な説明】
【０００９】
【図１】一実施形態におけるプログラム検証装置のハードウェア構成を示す図。
【図２】一実施形態におけるプログラム検証装置の機能ブロック図。
【図３】一実施形態における検証対象プログラムを示す図。
【図４】図２の検証対象プログラムに対する検証コードを示す図。
【図５】図３の検証コードをＳＰＩＮに従う検証コードに変換した状態を示す図。
【図６】一実施形態における検証データを示す図。
【図７】一実施形態におけるプログラム検証装置での検証処理のフロー図。
【図８】一実施形態における検証コードの合成処理のフロー図。
【図９】一実施形態における検証対象プログラムのソースコードを示す図。
【図１０】図９のソースコードに対応する３番地コードを示す図。
【図１１】図９及び１０の検証対象プログラムに対する検証コードを示す図。
【図１２】図１１の検証コードをＳＰＩＮに従う検証コードに変換した状態を示す図。
【図１３】一実施形態における検証データを示す図。
【図１４】一実施形態における検証対象プログラムを示す図。
【図１５】図１４の検証対象プログラムに対する検証コードを示す図。
【図１６】図１５の検証コードをＳＰＩＮに従う検証コードに変換した状態を示す図。
【図１７】一実施形態における検証データを示す図。
【発明を実施するための形態】
【００１０】
（第一実施形態）図１は、一実施形態におけるプログラム検証装置２０１のハードウェア構成を示す図である。例えば、ハードディスクといった外部記憶装置２０４には、検証対象プログラムと、検証装置用プログラムが保存されている。中央処理装置２０２は、検証装置用プログラムを主記憶装置２０３にロードして実行することで、以下に説明する様なプログラム検証装置２０１が実現される。つまり、プログラム検証装置２０１は、コンピュータを以下に説明するプログラム検証装置２０１として機能させるプログラムにより実現することができる。プログラム検証装置２０１は、検証対象プログラムの言語仕様のうちの検証対象の仕様である検証対象仕様を、検証対象プログラムが満足しているか否かの検証を行う。なお、入出力装置２０５は、例えば、ディスプレイ等の表示装置や、キーボードやマウスなどの入力装置を含み、プログラム検証装置２０１に対するユーザの指示等の入力処理や、検証結果のユーザへの表示等の出力処理を行う。
【００１１】
以下、検証対象プログラムがＣ言語で記述されており、検証対象仕様が、“配列外へのメモリアクセスは行ってはならない”（以後、配列外参照と呼ぶ。）と、“０による割り算を実行してはならない”（以後、ＤＩＶ０と呼ぶ。）である場合を例にして説明を行う。なお、プログラム検証装置２０１が実行する検証コードはＳＰＩＮで記述されているものとする。
【００１２】
図２は、本実施形態によるプログラム検証装置２０１の機能ブロック図である。検証式生成部３０３は、検証対象プログラム３０９の処理内容を解析し、検証対象仕様を満たすか否かを判定するための検証式を生成して検証データ３１０として出力する。
【００１３】
図３に、本実施形態の説明に使用する検証対象プログラム３０９を示す。なお、図３(ａ)はＣ言語で記述されたソースコードを、図３（ｂ）は、図３（ａ）のソースコードを、静的単一代入形式（ＳＳＡ）といった、３番地コードに変換したものを示している。なお、ソースコードから３番地コードへの変換は公知の種々の方法を利用することができる。例えば、検証式生成部３０３は、図３(ａ)に示すソースコードを、まず、図３（ｂ）に示す３番地コードに変換する。検証式生成部３０３は、その後、ソースコード及び３番地コードに基づき、検証対象仕様に対応する処理部分を判定し、各処理部分それぞれについて検証式を生成する。
【００１４】
具体的には、図３に示す検証対象プログラムから以下の内容を把握することできる。
・図３（ｂ）の関数ｔｅｓｔ１のｌｉｎｅ１において、ｐｒｍを添え字にして、配列ｖａｒにアクセスする。
・第３（ｂ）の関数ｔｅｓｔ１のｌｉｎｅ３において、Ｄ．１１８５による割り算を実行する。なお、ｌｉｎｅ２よりＤ．１１８５はｐｒｍ＋１に等しい。
・ｐｒｍはｔｅｓｔ１の引数であり、関数ｔｅｓｔ１のｌｉｎｅ１〜ｌｉｎｅ３の間で変更されない。
・図３（ａ）から配列ｖａｒの要素数は３である。
【００１５】
上記内容から、関数ｔｅｓｔ１に関し、配列外参照に対応する処理部分は、ｌｉｎｅ１であり、ｌｉｎｅ１の配列ｖａｒへのアクセスにおいて、ｐｒｍが０以上３未満であることを検証すれば良いことが分かる。つまり、ｌｉｎｅ１の処理部分に対する配列外参照の検証式は、（０＜＝ｐｒｍ＆＆ｐｒｍ＜３）となる。同様に、ＤＩＶ０に対応する処理部分はｌｉｎｅ３であり、ｌｉｎｅ３におけるＤ．１１８５＝ｐｒｍ＋１が０以外であることを検証すれば良いことが分かる。つまり、ＤＩＶ０に対する検証式は、（ｐｒｍ＋１！＝０）となる。
【００１６】
従って、検証式生成部３０３は、図６（ａ）に示す検証データ３１０を出力する。図６(ａ)において、検証ＩＤフィールドは、検証式の識別子を示し、関数名フィールドは検証対象の関数名を示し、行番号フィールドは、検証対象仕様に対応する処理部分であり、図３（ｂ）の三番地コードの行番号で示している。また、検証式フィールドは、検証対象仕様に対応する検証式を示し、コード生成フィールドは、検証コードを既に生成したか否かを示している。この時点において検証コードは生成されていないため、コード生成フィールドには“ｎｏ”が設定されている。さらに、コードＮｏフィールドは、検証コードを生成した場合においてその番号を示し、検証結果フィールドは、検証式が検証対象仕様を満足しているか否かを示す。
【００１７】
図２に戻り、検証コード生成部３０４は、図６（ａ）に示す検証データ３１０及び図３に示す検証対象プログラムから、検証対象仕様である配列外参照とＤＩＶ０それぞれを検証するための検証コード３１１を生成する。各検証コード３１１の生成には、公知のコードスライス法を利用できる。つまり、検証対象プログラムの依存関係を調べ、検証対象仕様に関連する値に影響する検証対象プログラムのコードのみを残し、それ以外の部分を消去して検証式を埋め込むことにより、検証コード生成部３０４は検証コード３１１を生成する。図４(ａ)は、図６（ａ）の検証ＩＤ＃１の検証式に対応する検証コード３１１であり、図４(ｂ)は、図６（ａ）の検証ＩＤ＃２の検証式に対応する検証コード３１１である。図４（ａ）に示す様に、検証ＩＤ＃１に対応する検証コード３１１は、図３（ｂ）の関数ｔｅｓｔ１の当該検証式に関連するｌｉｎｅ１のｐｒｍ値に影響するコードのみを残すことで生成されている。また、検証コード生成部３０４は、検証コードを生成したことにより、図６(ｂ)に示す様に、検証データのコード生成フィールドを“ｙｅｓ”に設定し、コードＮｏフィールドに対応する番号を設定する。
【００１８】
続いて、検証コード合成部３０５は、各関数について、検証コードの合成処理を行う。合成処理の詳細については、後述するが、図４（ａ）及び（ｂ）に示す２つの検証コードが使用する変数は同じであるため、合成可能である。検証コード合成部３０５が出力する合成後の検証コード３１２を図４（ｃ）に示す。なお、図４（ｃ）では、各ａｓｓｅｒｔ文を順に記述しているが、（０！＝ｐｒｍ＋１）＆＆（０＜＝ｐｒｍ＆＆ｐｒｍ＜３）の様に、一つの検証式としても良い。また、検証コード合成部３０５は、検証コードを生成したことにより、図６(ｃ)に示す様に、コードＮｏフィールドに対応する番号を設定する。
【００１９】
次に、変換部３０６は、検証コード３１１又は３１２を、プログラム検証装置がサポートするモデル検証用の言語に対応する検証コード３１３に変換する。より詳しくは、検証コード合成部３０５により合成された検証式については合成後の検証コード３１２を、合成されなかった検証式については検証コード３１１を、それぞれ、検証コード３１３に変換する。図５(ａ)は、モデル検証用の言語がＳＰＩＮである場合における図４（ｃ）の検証コード３１２の変換後の状態を示している。図５(ａ)に示す検証コード３１３により、検証領域を関数内に限定した検証を行う事が可能となる。
【００２０】
検証実行部３０７は、検証コード３１３を読み込んで検証式を満たすか否かを判定し、判定結果を検証データ３１０の検証結果フィールドに設定する。ここで、検証対象仕様を満たしていない（ＮＧ）場合、制御部３０８は、スコープ外変数の存在を判定する。つまり、対象としている関数単体では、その値が不定となる変数の存在を判定する。図３に示す検証対象プログラムの関数ｔｅｓｔ１(第１の関数）において、ｐｒｍはスコープ外変数であり、その値が判定できないため、検証実行部３０７は、図５（ａ）の検証コード３１３についてはＮＧと判定することになる。この場合、制御部３０８は、当該関数と関連する他の関数を特定し、これら関連する関数にまで検証範囲を広げて、再度、上述した処理を実行する様に、図２の各部を制御する。図３（ｂ）に示す様に、関数ｔｅｓｔ１Ａ（第２の関数）のｌｉｎｅ４で関数ｔｅｓｔ１の呼び出しが行われているため、制御部３０８は、関数ｔｅｓｔ１Ａが、関数ｔｅｓｔ１と関連すると判定する。よって、制御部３０８は、２回目の実行において、関数ｔｅｓｔ１及びｔｅｓｔ１Ａを１つの検証範囲とする。図５（ｂ）に関数ｔｅｓｔ１及びｔｅｓｔ１Ａを検証範囲に加えた場合の検証コード３１３を示す。図５（ｂ）の検証コード３１３については、検証対象仕様を満たしている（ＯＫ）ため、検証実行部３０７は、図６（ｄ）に示す様に検証結果フィールドにＯＫを設定する。
【００２１】
続いて、図７及び８を用いて、本実施形態によるプログラム検証処理について説明する。図７のＳ１において、検証式生成部３０３は、検証対象プログラム３０９の処理内容を解析し、検証対象仕様に関係する処理部分毎に、図６に示す様な検証式を生成する。Ｓ２において、検証コード生成部３０４は、各関数の各検証式を検証するための必要最小限の検証コード３１１を生成する。つまり、検証コード生成部３０４は、検証式生成部３０３が生成した検証式毎に検証コード３１１を生成する。図４(ａ)及び（ｂ）に示す検証コード３１１の生成には、公知のコードスライス法を利用できる。
【００２２】
続いて、Ｓ３において、検証コード合成部３０５は、各関数についての検証コード３１１の合成処理を行う。図８は検証コード合成部３０５による合成処理のフロー図である。なお、図８の処理は各関数について実行する。Ｓ１１において、検証コード合成部３０５は、検証データ３１０から、同じ関数内の２つの検証コード３１１を処理対象として選択する。例えば、図６に示す検証データ３１０においては、検証ＩＤ＃１及び＃２で特定される２つの検証コード３１１を処理対象として選択する。Ｓ１２において、検証コード合成部３０５は、各検証コード３１１の変数が包含関係にあるか否かを判定する。包含関係とは、一方の検証コード３１１の変数の総てが、他方の検証コード３１１においても変数として使用されている状態を意味する。なお、変数の異同は、名前及び型が同じ場合に変数が同じであると判定する。包含関係になければ、検証コード合成部３０５は、選択した２つの検証コード３１１の合成は不可と判定して処理を終了する。一方、包含関係にあれば、検証コード合成部３０５は、Ｓ１３において、各検証コード３１１の変数が同じであり、かつ、検証式以外のコード部分が同一であるかを判定する。変数が同じであり、かつ、検証式以外のコード部分が同一である場合、検証コード合成部３０５は、Ｓ１４において、検証式の合成を行うことで、合成した検証コード３１２を生成する。一方、変数又は検証式以外のコード部分が同一ではない場合、検証コード合成部３０５は、Ｓ１５において、単に、選択した検証コード３１１の合成を行う。例えば、図４（ａ）及び（ｂ）に示す検証コード３１１で使用されている変数ｐｒｍは、その名前及び型（整数：ｉｎｔ）が同じであるので、同一である。また、検証式、つまり、ａｓｓｅｒｔ文以下のコード部分は同一（より詳しくは、ａｓｓｅｒｔ文のみである）であるため、Ｓ１３の処理は“Ｙｅｓ”である。
【００２３】
なお、Ｓ１３の判定はオプションであり、Ｓ１２の判定が“Ｙｅｓ”であれば、検証コード３１１は合成可能である。検証コード合成部３０５は、ある関数に対して３つ以上の検証コード３１１が有る場合、例えば、Ｓ１１においてそのすべてを選択し、Ｓ１２〜Ｓ１５の処理で合成可能な組を判定して合成後の検証コード３１２を生成することができる。あるいは、１つの注目する検証コード３１１に対して、他の１つの検証コード３１１を選択して図８の処理を繰り返して３つ以上の検証コードを合成することもできる。この場合、先の処理で注目する検証コード３１１を合成して、合成後の検証コード３１２を生成した場合、続く図８のＳ１１では、合成後の検証コード３１２と、次の検証コード３１１を選択する。一方、先の処理で注目する検証コード３１１が合成不可であれば、続く図８のＳ１１では、この注目する検証コード３１１と、次の検証コード３１１を選択して処理を行うことになる。いずれにしても、各関数内において、検証コードの合成を行う。
【００２４】
図７に戻り、Ｓ４において、変換部３０６は、検証コード３１１及び／又は３１２を、利用するモデル検証プログラム言語に従う検証コード３１３に変換し、検証実行部３０７が検証コード３１３を読み込んで、検証対象仕様を満足しているか否かを判定する。Ｓ５において、制御部３０８は、判定結果がどちらであるかを判定し、結果をＯＫであれば処理を終了する。一方、判定結果がＮＧであれば、Ｓ６において、スコープ外変数が存在するかを判定する。スコープ外変数が存在しない場合、制御部３０８は、処理を終了させるが、スコープ外変数が存在する場合、Ｓ７において検証コードの生成の対象とする検証範囲を拡大して、Ｓ１からの処理を実行する。なお、検証コードの生成の対象とする検証範囲を拡大するとは、既に説明した様に、判定結果がＮＧとなった関数と関連する他の関数を含めて、この互いに関連する複数の関数に対してＳ１からＳ７の処理を実行することを意味する。つまり、２回目以降の繰り返しにおいて、検証コード生成部３０４は、検証範囲に含まれる複数の関数を考慮してコードスライスを実行することになる。
【００２５】
以上、本実施形態においては、関数内で検証コードの合成を行った後に、まず、検証を行う。その後、検証結果がＮＧである場合、その範囲を増大させながら繰り返し検証を行うことで状態数を増加させることなく、確実にプログラム検証を行うことを可能にする。例えば、図２に示す検証対象プログラムにおいて、従来の様に、関数内における合成を行わないものとすると、４回の検証を行う必要がある。これに対して、本実施形態においては、関数内の検証コード３１１を合成することで、２回の検証のみで検証結果を取得できる。この様に、本実施形態による構成により検証時間を短縮することができる。なお、検証に用いる変数は合成前後で変化しないため、合成する事によって状態数の増加を引き起こす可能性は少ない。
【００２６】
（第二実施形態）第一実施形態においては、図８のＳ１２及びＳ１３の判定は共に“Ｙｅｓ”であった。以下、Ｓ１２の判定は“Ｙｅｓ”であるが、Ｓ１３の判定が“Ｎｏ”である場合について説明する。
【００２７】
図９は、検証対象プログラム３０９のソースコードを、図１０は、図９のソースコードに対応する３番地コードを示している。図９及び図１０の検証対象プログラム３０９から以下の内容を把握することできる。
・図１０の関数ｔｅｓｔ２のｌｉｎｅ２において、ｐｒｍを添え字にして、配列ｖａｒにアクセスする。
・図１０の関数ｔｅｓｔ２のｌｉｎｅ１２において、ｐｒｍを添え字にして、配列ｖａｒ２にアクセスする。
・ｐｒｍはｔｅｓｔ２の引数であり、関数ｔｅｓｔ２のｌｉｎｅ１〜ｌｉｎｅ１２の間で変更されない。
・図９から配列ｖａｒ及びｖａｒ２の要素数は３である。
【００２８】
上記内容から、関数ｔｅｓｔ２に関し、配列外参照に対しては、ｌｉｎｅ２及び１２における配列ｖａｒ及びｖａｒ２へのアクセスにおいて、ｐｒｍが０以上３未満であることを検証すれば良いことが分かる。従って、検証式生成部３０３は、図１３（ａ）に示す検証データ３１０を出力する。
【００２９】
検証コード生成部３０４は、図１３（ａ）に示す検証データ３１０から、検証ＩＤ＃１の検証式に対しては、図１１（ａ）に示す検証コード３１１を、検証ＩＤ＃２の検証式に対しては、図１１（ｂ）に示す検証コード３１１を生成する。また、検証コード３１１を生成したことにより、図１３(ｂ)に示す様に、検証データのコード生成フィールドを“ｙｅｓ”に設定し、コードＮｏフィールドに対応する番号を設定する。
【００３０】
続いて、検証コード合成部３０５は、各関数について、検証コードの合成処理を行う。図１１（ａ）及び図１１（ｂ）の検証コード３１１で使用する変数名は共にｐｒｍであり、その型は共に整数であるため、図８のＳ１２は“Ｙｅｓ”となる。しかしながら、図１１（ａ）の検証式を除いたコード部分、つまり、ｌｉｎｅ１−２以外の部分と、図１１（ｂ）の検証式を除いたコード部分、つまり、ｌｉｎｅ２−１０以外の部分は異なる。したがって、図８のＳ１３は“Ｎｏ”となる。しかしながら、図１１（ｂ）の検証コード（第１の検証コード）の検証式以外のコード部分は、図１１（ａ）の検証コード（第２の検証コード）の検証式以外のコード部分を包含している。つまり、ｌｉｎｅ１−１、１−３〜１−６は、ｌｉｎｅ２−１、２−２、２−３、２−４、２−１１に対応する。したがって、検証コード合成部３０５は、図１１（ａ）のｌｉｎｅ１−２の検証式であるａｓｓｅｒｔ分を、単に、図１１（ｂ）のｌｉｎｅ１−２に対応する、ｌｉｎｅ２−１と２−２の間に挿入することで、図１１（ｃ）に示す検証コード３１２へと合成する。また、検証コード合成部３０５は、合成した検証コード３１２を生成したことにより、図１３(ｃ)に示す様に、コードＮｏフィールドに対応する番号を設定する。
【００３１】
以下、変換部３０６は、検証コード３１２を、プログラム検証装置がサポートするモデル検証用の言語に対応する検証コード３１３に変換する。図１２(ａ)は、モデル検証用の言語がＳＰＩＮである場合における図１１（ｃ）の検証コード３１２の変換後の状態を示している。図９及び１０に示す検証対象プログラムの関数ｔｅｓｔ２において、ｐｒｍはスコープ外変数であるため、検証実行部３０７は、図１２（ａ）の検証コード３１３についてはＮＧと判定する。したがって、制御部３０８は、検証範囲を広げて、再度、上述した処理を実行する様に、図２の各部を制御する。
【００３２】
図１０に示す様に、関数ｔｅｓｔ２Ａのｌｉｎｅ５でｔｅｓｔ２関数の呼び出しが行われているため、２回目の実行において、関数ｔｅｓｔ２Ａを検証範囲に加える。図１２（ｂ）に関数ｔｅｓｔ２Ａを検証範囲に加えた場合の検証コード３１３を示す。図１２（ｂ）の検証コード３１３については、検証対象仕様を満たしている（ＯＫ）ため、検証実行部３０７は、図１３（ｄ）に示す様に検証結果フィールドにＯＫを設定する。
【００３３】
（第三実施形態）続いて、配列の添え字や割り算の分母が定数ではなく変数である場合について説明する。
【００３４】
図１４(ａ)は、検証対象プログラム３０９のソースコードを、図１４(ｂ)は、図１４(ａ)のソースコードに対応する３番地コードを示している。図１４(ａ)及び（ｂ）の検証対象プログラム３０９から以下の内容を把握することできる。
・図１４（ｂ）の関数ｔｅｓｔ３のｌｉｎｅ５においてＤ．１１２８による割り算を実行する。
・図１４（ｂ）の関数ｔｅｓｔ３のｌｉｎｅ６においてｓｙｍを添え字にして、配列ｖａｒにアクセスする。
・図１４（ａ）からｖａｒの配列要素数は３である。
【００３５】
上記内容から、関数ｔｅｓｔ３に関し、ＤＩＶ０に対しては、ｌｉｎｅ５におけるＤ．１１２８が０でないこと、配列外参照に対しては、ｌｉｎｅ６における配列ｖａｒへのアクセスにおいて、ｓｙｍが０以上３未満であることを検証すれば良いことが分かる。従って、検証式生成部３０３は、図１７（ａ）に示す検証データ３１０を出力する。
【００３６】
検証コード生成部３０４は、図１７（ａ）に示す検証データ３１０から、検証ＩＤ＃１の検証式に対しては、図１５（ａ）に示す検証コード３１１を、検証ＩＤ＃２の検証式に対しては、図１５（ｂ）に示す検証コード３１１を生成する。また、検証コード３１１を生成したことにより、図１７(ｂ)に示す様に、検証データのコード生成フィールドを“ｙｅｓ”に設定し、コードＮｏフィールドに対応する番号を設定する。
【００３７】
続いて、検証コード合成部３０５は、各関数について、検証コードの合成処理を行う。図１５（ａ）の検証コード３１２で使用する変数はＤ．１２２８及びｉであり、図１５（ａ）の検証コード３１２で使用する変数はＤ．１２２８、ｉ及びｓｙｍであり包含関係にある。よって、図８のＳ１２は“Ｙｅｓ”となる。しかしながら、図１５（ａ）の変数及び検証式を除いたコード部分、つまり、ｌｉｎｅ１−５以外の部分と、図１５（ｂ）の検証式以外のコード部分、つまり、ｌｉｎｅ２−６以外の部分は異なる。したがって、図８のＳ１２は“Ｎｏ”となる。
【００３８】
この場合、検証コード合成部３０５は、図８のＳ１５において合成処理を行い、図１６(ａ)に示す合成した検証コード３１２を生成する。なお、第二実施形態と同様に図１５（ｂ）の検証コードの検証式、つまり、ｌｉｎｅ２−６以外の部分は、図１５（ａ）の検証コードの検証式、つまり、ｌｉｎｅ１−５以外の部分を包含するものである。よって、合成処理は、図１５（ａ）の検証コードのｌｉｎｅ１−５の検証式を、図１５（ｂ）の検証コードの対応する位置、つまり、ｌｉｎｅ２−４と２−５の間に挿入することにより行われる。また、合成した検証コード３１２を生成したことにより、図１７(ｃ)に示す様に、コードＮｏフィールドに対応する番号を設定する。
【００３９】
以下、変換部３０６は、検証コード３１２を、プログラム検証装置がサポートするモデル検証用の言語に対応する検証コード３１３に変換する。図１６(ｂ)は、モデル検証用の言語がＳＰＩＮである場合における図１６（ａ）の検証コード３１２の変換後の状態を示している。検証実行部３０７は、図１６（ｂ）の検証コード３１３についてはＯＫと判定し、図１７（ｄ）に示す様に検証結果フィールドにＯＫを設定する。
【００４０】
以上、検証式に対応する検証コードを生成し、合成可能であるものについては複数の検証コードを１つの検証コードに合成することで、プログラム検証に要する時間を短縮化することができる。また、同じ関数内の検証コードに対して合成可能であるか否かを判定することで、簡易に判定して検証コードを合成することができる。なお、検証コードがスコープ外変数を有する場合、この検証コードに対応する関数を呼び出す関数を含める形で、検証コードを生成して、再度検証を行うことでプログラムの検証を行う。これにより、状態数の急激な増加を抑えつつ、プログラムの検証を行うことができる。
、なお、検証コードの合成は、２つの検証コードの対応する関数が同一であり、かつ、少なくとも２つの検証コードで使用されている変数が包含関係にある場合に合成可能であると判定する。なお、変数が同一であり、２つの検証コードの検証式を除いた部分が同一である場合、２つの検証コードの検証式を合成して１つの検証式にすることができる。また、一方の検証コードの検証式及び変数を除いた部分が、他方の検証コードの検証式及び変数を除いた部分を包含する場合、他方の検証コードの検証式を、一方の検証コードに挿入することにより検証コードの合成を行うことができる。この様に、検証コードの合成処理は、簡易であり、検証すべき状態数を効果的に減少させることができる。
【図１】
2012238235.tif 000003
【図２】
2012238235.tif 000004
【図３】
2012238235.tif 000005
【図４】
2012238235.tif 000006
【図５】
2012238235.tif 000007
【図６】
2012238235.tif 000008
【図７】
2012238235.tif 000009
【図８】
2012238235.tif 000010
【図９】
2012238235.tif 000011
【図１０】
2012238235.tif 000012
【図１１】
2012238235.tif 000013
【図１２】
2012238235.tif 000014
【図１３】
2012238235.tif 000015
【図１４】
2012238235.tif 000016
【図１５】
2012238235.tif 000017
【図１６】
2012238235.tif 000018
【図１７】
2012238235.tif 000019