(57)【要約】【課題】モデル検査技法を利用してソースコードの検証を行う処理系において、検証効果が高くなる関数を自動選択する。【解決手段】モデル検査を実行する前に、任意値をとる変数や関数の返却値を利用して、検証対象のモデルの再構築を行うことにより、与えられた検証時間内により有効な検証結果が得られるモデルを出力する。まず、与えられたソースコードから変換されたＣＦＧモデルにおいて、任意値を取る変数や関数の参照を含む一連の関数呼び出しフローを検査対象から除外する。更に、呼び出し上位の関数に対して、下位の関数がどれだけ多くのコンテキストを与えているか、つまり下位関数をモデル化することで、どれだけ上位関数の検証精度が高くなるかという基準で、ランク付けを行った上で、再構築するモデルの全体ブロック数が、事前に指定された上限の範囲内に収まるように関数の取捨選択を行う。【選択図】図１
2010211521.tif 000002
【特許請求の範囲】
【請求項１】
検査仕様と検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成するモデル検査制御手段と、
前記ＣＦＧモデルを読み込み、前記検査仕様で指定されたエントリ関数から呼び出される関数を検出し、前記検出された関数のブロック数と評価値を算出し、前記算出されたブロック数と評価に基づいて、前記検出された関数の中から、検証対象に追加する関数を選択し、前記選択された関数に基づいて、前記ＣＦＧモデルを変換する検証対象関数選択手段と
を含み、
前記モデル検査制御手段は、前記変換されたＣＦＧモデルを読み込み、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、前記検査モデルに対して、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、前記実行された検査の結果を出力する
検証対象関数自動選択装置。
【請求項２】
請求項１に記載の検証対象関数自動選択装置であって、
前記モデル検査制御手段は、
前記検査仕様と前記検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧモデルを作成するＣＦＧモデル作成手段と、
前記変換されたＣＦＧモデルを読み込み、計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成する検査モデル作成手段と、
前記検査モデルを読み込み、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行するモデル検査実行手段と、
前記記号モデル検査実行手段が実行した検査の結果を出力する検査結果出力手段と
を含む
検証対象関数自動選択装置。
【請求項３】
請求項１又は２に記載の検証対象関数自動選択装置であって、
前記検証対象関数選択手段は、
前記ＣＦＧモデルを読み込み、前記検査仕様で指定されたエントリ関数から直接的又は間接的に呼び出される関数全てを検出する呼び出し関数検出手段と、
前記呼び出し関数検出手段が検出した関数のそれぞれに対し、当該関数のブロック数と評価値を算出する関数評価手段と、
前記検査仕様に指定された最大ブロック数の範囲内で、評価値の高い関数を選択する検証対象関数選択手段と、
前記検証対象関数選択手段が選択した関数以外の関数を前記ＣＦＧモデルから削除し、前記選択された関数が関数として残されたＣＦＧモデルを、前記変換されたＣＦＧモデルとして出力するＣＦＧモデル変換手段と
を含む
検証対象関数自動選択装置。
【請求項４】
検査仕様と検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成するＣＦＧモデル作成手段と、
前記ＣＦＧモデルを読み込み、前記検査仕様で指定されたエントリ関数から呼び出される関数を検出する呼び出し関数検出手段と、
前記呼び出し関数検出手段が検出した関数のそれぞれに対し、当該関数のブロック数と評価値を算出する関数評価手段と、
前記検査仕様に指定された最大ブロック数の範囲内で、評価値の高い関数を選択する検証対象関数選択手段と、
前記検証対象関数選択手段が選択した関数に基づいて、前記ＣＦＧモデルを変換して前記変換されたＣＦＧモデルを生成するＣＦＧモデル変換手段と、
前記変換されたＣＦＧモデルを読み込み、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成する検査モデル作成手段と、
前記検査モデルを読み込み、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行するモデル検査実行手段と、
前記記号モデル検査実行手段が実行した検査の結果を出力する検査結果出力手段と
を含む
検証対象関数自動選択装置。
【請求項５】
検査仕様と検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成し、
前記ＣＦＧモデルを参照し、前記検査仕様で指定されたエントリ関数から呼び出される関数を検出し、前記検出された関数のブロック数と評価値を算出し、前記算出されたブロック数と評価に基づいて、前記検出された関数の中から、検証対象に追加する関数を選択し、前記選択された関数に基づいて、前記ＣＦＧモデルを変換し、
前記変換されたＣＦＧモデルを参照し、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、前記検査モデルに対して、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、前記実行された検査の結果を出力する
検証対象関数自動選択方法。
【請求項６】
請求項５に記載の検証対象関数自動選択方法であって、
前記検査仕様と前記検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧモデルを作成し、
前記変換されたＣＦＧモデルを読み込み、計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、
前記検査モデルを読み込み、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、
前記実行された検査の結果を出力する
検証対象関数自動選択方法。
【請求項７】
請求項５又は６に記載の検証対象関数自動選択方法であって、
前記ＣＦＧモデルを読み込み、前記検査仕様で指定されたエントリ関数から直接的又は間接的に呼び出される関数全てを検出し、
前記検出された関数のそれぞれに対し、当該関数のブロック数と評価値を算出し、
前記検査仕様に指定された最大ブロック数の範囲内で、評価値の高い関数を選択し、
前記選択された関数以外の関数を前記ＣＦＧモデルから削除し、前記選択された関数が関数として残されたＣＦＧモデルを、前記変換されたＣＦＧモデルとして出力する
検証対象関数自動選択方法。
【請求項８】
検査仕様と検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成し、
前記ＣＦＧモデルを読み込み、前記検査仕様で指定されたエントリ関数から呼び出される関数を検出し、
前記検出された関数のそれぞれに対し、当該関数のブロック数と評価値を算出し、
前記検査仕様に指定された最大ブロック数の範囲内で、評価値の高い関数を選択し、
前記選択された関数に基づいて、前記ＣＦＧモデルを変換して前記変換されたＣＦＧモデルを生成し、
前記変換されたＣＦＧモデルを読み込み、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、
前記検査モデルを読み込み、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、
前記実行された検査の結果を出力する
検証対象関数自動選択方法。
【請求項９】
検査仕様と検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成するステップと、
前記ＣＦＧモデルを参照し、前記検査仕様で指定されたエントリ関数から呼び出される関数を検出し、前記検出された関数のブロック数と評価値を算出し、前記算出されたブロック数と評価に基づいて、前記検出された関数の中から、検証対象に追加する関数を選択し、前記選択された関数に基づいて、前記ＣＦＧモデルを変換するステップと、
前記変換されたＣＦＧモデルを参照し、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、前記検査モデルに対して、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、前記実行された検査の結果を出力するステップと
をコンピュータに実行させるための
検証対象関数自動選択用プログラム。
【請求項１０】
請求項９に記載の検証対象関数自動選択用プログラムであって、
前記検査仕様と前記検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧモデルを作成するステップと、
前記変換されたＣＦＧモデルを読み込み、計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成するステップと、
前記検査モデルを読み込み、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行するステップと、
前記実行された検査の結果を出力するステップと
を更にコンピュータに実行させるための
検証対象関数自動選択用プログラム。
【請求項１１】
請求項９又は１０に記載の検証対象関数自動選択用プログラムであって、
前記ＣＦＧモデルを読み込み、前記検査仕様で指定されたエントリ関数から直接的又は間接的に呼び出される関数全てを検出するステップと、
前記検出された関数のそれぞれに対し、当該関数のブロック数と評価値を算出するステップと、
前記検査仕様に指定された最大ブロック数の範囲内で、評価値の高い関数を選択するステップと、
前記選択された関数以外の関数を前記ＣＦＧモデルから削除し、前記選択された関数が関数として残されたＣＦＧモデルを、前記変換されたＣＦＧモデルとして出力するステップと
を更にコンピュータに実行させるための
検証対象関数自動選択用プログラム。
【請求項１２】
検査仕様と検査対象コードを読み込み、前記検査対象コードにコンパイラ最適化処理を施した上で、前記検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成するステップと、
前記ＣＦＧモデルを読み込み、前記検査仕様で指定されたエントリ関数から呼び出される関数を検出するステップと、
前記検出された関数のそれぞれに対し、当該関数のブロック数と評価値を算出するステップと、
前記検査仕様に指定された最大ブロック数の範囲内で、評価値の高い関数を選択するステップと、
前記選択された関数に基づいて、前記ＣＦＧモデルを変換して前記変換されたＣＦＧモデルを生成するステップと、
前記変換されたＣＦＧモデルを読み込み、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成するステップと、
前記検査モデルを読み込み、前記計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行するステップと、
前記実行された検査の結果を出力するステップと
をコンピュータに実行させるための
検証対象関数自動選択用プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検証対象関数自動選択装置に関し、特にモデル検査手法における検証対象関数自動選択装置に関する。
【背景技術】
【０００２】
Ｃ言語を始めとするプログラミング言語で記述されたソースコードを、形式検証の一手法であるモデル検査技法で検証するための方法として、例えば、“情報処理  ４９（５）「Ｃ言語へのフォーマルメソッドの適用」宮崎義昭、橋本祐介著（非特許文献１）”に記載されている従来技術のように、従来からいくつかの方法が知られている。
【０００３】
また、関連技術として、特表２００７−５２８０５９号公報（特許文献１）にソフトウェアのモデル化、抽象、及び分析のためのシステムと方法が開示されている。
【０００４】
この関連技術は、ソースコード検証においてソースコードをモデル検査可能なモデルに変換し検証を行う技術である。
【０００５】
しかし、この関連技術では、モデル化する関数に関しては何ら特別な処理は行わず、利用者が指定した検証コード及び検証対象の起点となる関数（エントリ関数と呼ぶ）から直接又は間接的に呼び出される関数全てを検証対象に加えていた。このため、検証結果が出てからでないと制限時間切れで検証結果が出ていないことがわからず、それを回避するための関数選択で人手による試行錯誤が必要となっていた。またその試行錯誤でも勘に頼った方法をとっていたため、必ずしも意図した通りの設定にすることができないという問題があった。
【０００６】
一般に、ソースコードから自動的にモデルを構築し、モデル検査による検証を行う場合、生成されるモデルの状態数が膨大になり、計算量が非常に多くなるため、有意な時間内で全ての検証が終了しない場合が多い。
【０００７】
そのため、検証時間の上限を予め設定しておき、その時間内で結果が得られない検証項目については、タイムアウトとして検証を終了する方法が取られている。
【０００８】
また、出来るだけ多くの検証結果が得られるように、モデル化の過程で様々な最適化を行い、検証結果に影響を与えない範囲でモデルを小さくする処理を行っているが、従来のモデル構築方法では、利用者が指定した起点関数から直接又は間接的に呼び出される関数を全て検証対象に加える方法を取っているため、対象となる関数が多い場合には、上限時間内に検証結果を出せない場合も多い。
【０００９】
このような場合、起点関数から直接又は間接的に呼び出される関数のうち、計算量が多く制限時間内に結果が得られない一部の関数の検証に多くの時間が費やされ、比較的短い時間で検証が可能なその他の関数の検証にも影響が及び、全体として効果的な検証時間の配分がされていないという課題があった。
【先行技術文献】
【特許文献】
【００１０】
【特許文献１】特表２００７−５２８０５９号公報
【非特許文献】
【００１１】
【非特許文献１】情報処理  ４９（５）「Ｃ言語へのフォーマルメソッドの適用」宮崎義昭、橋本祐介著
【非特許文献２】「コンパイラＩＩ  原理・技法・ツール」Ａ．Ｖ．エイホ、Ｒ．セシィ、  Ｊ．Ｄ．ウルマン著
【非特許文献３】産業技術総合研究所システム検証研究センター、テクニカルレポート「抽象化を用いた検証ツールの調査」田辺良則、高井利憲、高橋孝一
【発明の概要】
【発明が解決しようとする課題】
【００１２】
本発明の目的は、モデル検査を実行する前に、検証対象のモデルの再構築を行うことにより、検証効果が高い関数群を自動的に選択してからモデル化する検証対象関数自動選択装置を提供することである。
【課題を解決するための手段】
【００１３】
本発明の検証対象関数自動選択装置は、検査仕様と検査対象コードを読み込み、検査対象コードにコンパイラ最適化処理を施した上で、検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成するモデル検査制御手段と、ＣＦＧモデルを読み込み、検査仕様で指定されたエントリ関数から呼び出される関数を検出し、検出された関数のブロック数と評価値を算出し、算出されたブロック数と評価に基づいて、検出された関数の中から、検証対象に追加する関数を選択し、選択された関数に基づいて、ＣＦＧモデルを変換する検証対象関数選択手段とを含む。
【００１４】
モデル検査制御手段は、変換されたＣＦＧモデルを読み込み、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、検査モデルに対して、計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、実行された検査の結果を出力する。
【００１５】
本発明の検証対象関数自動選択方法では、検査仕様と検査対象コードを読み込み、検査対象コードにコンパイラ最適化処理を施した上で、検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成する。次に、ＣＦＧモデルを参照し、検査仕様で指定されたエントリ関数から呼び出される関数を検出し、検出された関数のブロック数と評価値を算出し、算出されたブロック数と評価に基づいて、検出された関数の中から、検証対象に追加する関数を選択し、選択された関数に基づいて、ＣＦＧモデルを変換する。次に、変換されたＣＦＧモデルを参照し、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、検査モデルに対して、計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、実行された検査の結果を出力する。
【００１６】
本発明の検証対象関数自動選択用プログラムは、  検査仕様と検査対象コードを読み込み、検査対象コードにコンパイラ最適化処理を施した上で、検査仕様を踏まえてＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデルを作成するステップと、ＣＦＧモデルを参照し、検査仕様で指定されたエントリ関数から呼び出される関数を検出し、検出された関数のブロック数と評価値を算出し、算出されたブロック数と評価に基づいて、検出された関数の中から、検証対象に追加する関数を選択し、選択された関数に基づいて、ＣＦＧモデルを変換するステップと、変換されたＣＦＧモデルを参照し、計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、検査モデルに対して、計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行し、実行された検査の結果を出力するステップとをコンピュータに実行させるためのプログラムである。
【発明の効果】
【００１７】
モデル検査に先立って、検証対象のモデルの再構築を行うことにより、与えられた検証時間内により有効な検証結果が得られる。
【図面の簡単な説明】
【００１８】
【図１】本発明の検証対象関数自動選択装置の構成例を示すブロック図である。
【図２】本発明の検証対象関数自動選択装置の動作を示すフローチャートである。
【図３】評価値（Ｘ，Ｙ）の算出に用いられる規則の例を示す図である。
【図４】第１のエントリ関数の例を示す図である。
【図５】第１のエントリ関数の処理結果の例を示す図である。
【図６】第２のエントリ関数の例を示す図である。
【図７】第２のエントリ関数の処理結果の例を示す図である。
【図８】第３のエントリ関数の例を示す図である。
【図９】第３のエントリ関数の処理結果の例を示す図である。
【図１０】検証対象関数選択部の動作を示すフローチャートである。
【図１１】検証対象関数選択部による第１のエントリ関数の処理結果の例を示す図である。
【図１２】検証対象関数選択部による第２のエントリ関数の処理結果の例を示す図である。
【図１３】検証対象関数選択部による第３のエントリ関数の処理結果の例を示す図である。
【発明を実施するための形態】
【００１９】
＜本実施形態＞
以下に、本発明の実施形態について添付図面を参照して説明する。
図１に示すように、本発明の検証対象関数自動選択装置は、検査仕様１と検査対象コード（検査対象プログラム）２を入力し、検査結果３を出力する。
【００２０】
本発明の検証対象関数自動選択装置は、モデル検査制御部１０と、記憶装置２０と、検証対象関数選択部３０を含む。
【００２１】
モデル検査制御部１０は、ＣＦＧ（Ｃａｌｌ  Ｆｌｏｗ  Ｇｒａｐｈ：制御流れグラフ）モデル作成部１１と、検査モデル作成部１２と、モデル検査実行部１３と、検査結果出力部１４を含む。
【００２２】
記憶装置２０は、変換前ＣＦＧモデル記憶部２１と、変換後ＣＦＧモデル記憶部２２と、検査モデル記憶部２３を含む。
【００２３】
検証対象関数選択部３０は、呼び出し関数検出部３１と、関数評価部３２と、検証対象関数追加部３３と、ＣＦＧモデル変換部３４を含む。検証対象関数選択部３０は、本特許の特徴的な構成要素である。
【００２４】
ＣＦＧモデル作成部１１は、検査仕様１と検査対象コード２を読み込み、従来技術のコンパイラ最適化処理を実施した上でＣＦＧモデルを作成し、記憶装置２０の変換前ＣＦＧモデル記憶部２１に出力する。
【００２５】
ここで、検査仕様１は、検証対象の起点となる関数（エントリ関数）の名前、検証上限時間、及び検証方法等を指示するオプション類を含んでいる。更に、本発明においては、検査仕様１は、検証を行うモデルのＣＦＧ表現における最大ブロック数を含んでいる。
【００２６】
検査モデル作成部１２は、記憶装置２０の変換後ＣＦＧモデル記憶部２１からＣＦＧモデルを読み込み、従来技術である計算機論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ：ＣＴＬ）を用いた記号モデル検査法に即して検査モデルを作成し、記憶装置２０の検査モデル記憶部２３に出力する。
【００２７】
モデル検査実行部１３は、記憶装置２０の検査モデル記憶部２３から検査モデルを読み込み、上記の従来技術の計算機論理（ＣＴＬ）を用いた記号モデル検査法に即して検査を実行する。
【００２８】
検査結果出力部１４は、記号モデル検査実行部１２が実行した検査の結果を検査結果３として出力する。
【００２９】
呼び出し関数検出部３１は、記憶装置２０の変換前ＣＦＧモデル記憶部２１に保持されたＣＦＧモデルを読み込み、検査仕様１で指定されたエントリ関数から呼び出される関数を検出する。
【００３０】
関数評価部３２は、呼び出し関数検出部３１が検出した関数のそれぞれに対し、その関数のブロック数と評価値を算出する。
【００３１】
検証対象関数選択部３３は、検査仕様１に指定された最大ブロック数の範囲内で、評価値の高い関数を選択する。
【００３２】
ＣＦＧモデル変換部３４は、検証対象関数選択部３３が選択した関数からＣＦＧモデルが構成されるようにＣＦＧモデルを変換し、変換されたＣＦＧモデルを変換後ＣＦＧモデル記憶部２２に出力する。
【００３３】
＜本実施形態の動作の説明＞
次に、図２のフローチャートを参照して、本実施形態の動作について詳細に説明する。
【００３４】
（１）ステップＡ１
まず、ＣＦＧモデル作成部１１は、検査仕様１及び検査対象コード２を参照し、検査対象コード２にコンパイラ最適化処理を施した上で、検査仕様１を踏まえてＣＦＧモデルを作成し、このＣＦＧモデルを変換前ＣＦＧモデル記憶部２１に記憶する。コンパイラ最適化処理ならびにＣＦＧモデル作成処理は、例えば、“「コンパイラＩＩ  原理・技法・ツール」Ａ．Ｖ．エイホ、Ｒ．セシィ、  Ｊ．Ｄ．ウルマン著（非特許文献２）”に記載されているような従来技術で行う。
【００３５】
（２）ステップＡ２
次に、呼び出し関数検出部３１は、変換前ＣＦＧモデル記憶部２１に記憶されたＣＦＧモデルの中から、検査仕様１で指定されたエントリ関数から直接的又は間接的に呼び出される関数全てを検出する。
【００３６】
（３）ステップＡ３
次に、関数評価部３２は、検出された関数のブロック数と評価値を算出する。詳細については後述する。
【００３７】
（４）ステップＡ４
次に、検証対象関数選択部３３は、算出されたブロック数と評価に基づいて、検出された関数の中から、検証対象に追加する関数を選択する。
【００３８】
（５）ステップＡ５
次に、ＣＦＧモデル変換部３４は、選択された関数以外の関数をＣＦＧモデルから削除し、選択された関数のみ関数として残されたＣＦＧモデルを、変換後ＣＦＧモデル記憶部２２に記憶する。
【００３９】
（６）ステップＡ６
次に、検査モデル作成部１２は、変換後ＣＦＧモデル記憶部２２に記憶されたＣＦＧモデルから検査モデルを作成し、この検査モデルを検査モデル記憶部２３に記憶する。検査モデル作成処理は、例えば、“産業技術総合研究所システム検証研究センター、テクニカルレポート「抽象化を用いた検証ツールの調査」田辺良則、高井利憲、高橋孝一（非特許文献３）”に記載されているような従来技術で行う。
【００４０】
（７）ステップＡ７
モデル検査実行部１３は、検査モデル記憶部２３に記憶された検査モデルを読み込み、モデル検査を実施する。
【００４１】
（８）ステップＡ８
最後に、検査結果出力部１４は、モデル検査の結果を検査結果３として出力する。
【００４２】
ここで、ステップＡ３に関して、詳細に説明する。
関数評価部３２は、検出された関数の、ブロック数と評価値を算出する。このとき、関数のブロック数とは、その関数のＣＦＧ表現におけるブロック数とする。
【００４３】
また、関数の評価値は、任意値の参照の有無と、下位関数が上位関数に対する検証精度向上への影響度によりランク付けができる指標を設定するが、具体的な指標はモデル検査実行部１３の特性により異なるため、ここでは例を用いて説明する。
【００４４】
この例では、評価値（Ｘ，Ｙ）は、「Ｘ」と「Ｙ」の二つの値から構成されるものとする。
【００４５】
「Ｘ」は、その関数から呼び出される関数（下位関数と呼ぶ）が任意値を返すものとした場合に得られる評価値とする。また、「Ｙ」は、下位関数の評価値を踏まえて得られる評価値とする。
【００４６】
従って、下位関数がない場合、「Ｘ」と「Ｙ」は同じ値となる。これにより、下位関数が検証対象関数として選択されなかった場合の評価値が「Ｘ」、下位関数が検証対象関数として選択された場合の評価値が「Ｙ」とみなすことができる。
【００４７】
評価値（Ｘ，Ｙ）の算出には、図３の規則を用いる。
図３には、以下の３つの規則が示されている。
【００４８】
（１）規則１：関数の戻り値を上位関数で使用している場合
戻り値の計算式の中に直接又は間接に任意値を含む場合、０点加算する（点を加算しない）。
戻り値の計算式の中に直接又は間接に任意値を含まない場合、１点加算する。
【００４９】
（２）規則２：関数の引数がアドレス渡しの場合
関数内でその引数が指す先に代入している計算式の中に直接又は間接に任意値を含む場合、０点加算する（点を加算しない）。
関数内でその引数が指す先に代入している計算式の中に直接又は間接に任意値を含まない場合、引数１つにつき１点加算する。
【００５０】
（３）規則３：関数の大域変数の代入がある場合
その代入する計算式の中に間接的に任意値を含む場合、０点加算する（点を加算しない）。
その代入する計算式の中に間接的に任意値を含まない場合、大域変数１つにつき１点加算する。
【００５１】
この規則は、アドレス渡し引数及び大域変数の場合は、１つに付き１点加算する点が特徴である。その理由は、上位関数で影響を受ける変数の数が多いほど、検証に与える影響が大きいためである。
【００５２】
次に、図４から図９を参照して、関数評価部３２の動作を具体的に説明する。
【００５３】
図４を参照して、図３の規則１，規則２，規則３について説明する。
【００５４】
図４で、「ｅｎｔｒｙ１」がエントリ関数とする。「ｅｎｔｒｙ１」からは「ｆ１」，「ｆ２」，「ｆ３」の各関数が呼ばれている。
【００５５】
「ｆ１」の戻り値は、上位関数で使用されており、戻り値の計算式の中に直接又は間接に任意値を含まないため、図３の規則１により、評価値は「１」となる。
【００５６】
「ｆ２」のアドレス渡し引数は、２つとも「ｆ２」内で値が代入されており、２つとも「ｆ２」内でその引数が指す先に代入している計算式の中に直接又は間接に任意値を含まないため、図３の規則２により、評価値は「２」となる。
【００５７】
また、「ｆ３」の場合は、３つの大域変数に値が代入されており、その代入する計算式の中に直接又は間接に任意値を含まないため、図３の規則３により、評価値は「３」となる。
【００５８】
また、「ｆ１」，「ｆ２」，「ｆ３」は、下位関数を持たないため、評価値（Ｘ，Ｙ）の「Ｘ」と「Ｙ」は同じ値となる。
【００５９】
従って、「ｆ１」，「ｆ２」，「ｆ３」の評価値は、それぞれ（１，１），（２，２），（３，３）となる。
【００６０】
この結果を図示したのが図５である。
【００６１】
図５において、“「ｆ１」（１，１）：１８”は、関数「ｆ１」のブロック数は「１８」であり、評価値は（１，１）であることを意味する。同様に、“「ｆ２」（２，２）：２８”は、関数「ｆ２」のブロック数は「２８」であり、評価値は（２，２）であることを意味する。“「ｆ３」（３，３）：３８”は、関数「ｆ３」のブロック数は「３８」であり、評価値は（３，３）であることを意味する。ブロック数は、図６の例では具体的に示していないが、後述する検証対象関数選択部３３の動作を説明するために例として付与した値である。
【００６２】
次に、図６を参照して、図３の１の規則について説明する。
【００６３】
図６で、「ｅｎｔｒｙ２」がエントリ関数とする。「ｅｎｔｒｙ２」からは「ｇ１」，「ｇ４」，「ｇ６」の各関数が呼ばれている。また、「ｇ１」，「ｇ４」，「ｇ６」の各関数の戻り値は、上位関数「ｉ」，「ｊ」，「ｋ」で使用されている。
【００６４】
「ｇ１」，「ｇ２」，「ｇ３」，「ｇ４」は、下位関数を持つ。「ｇ５」，「ｇ６」は、下位関数を持たない。
【００６５】
ここで、「ｇ３」から呼ばれている下位関数「ｕｎｄｅｔ」は、検証対象コード２に含まれていない関数である。従って、「ｕｎｄｅｔ」の戻り値は、任意値である。「ｇ３」は、戻り値の計算式の中に、間接に任意値を含むため、評価値は「０」である。同様に、「ｇ２」、「ｇ１」は、それぞれ戻り値の計算式の中に、間接に任意値を含むことになるため、評価値は「０」である。
【００６６】
これに対し、「ｇ５」，「ｇ６」は、戻り値の計算式の中に、直接又は間接に任意値を含まないため、評価値は「１」である。同様に、「ｇ４」は、それぞれ戻り値の計算式の中に、間接に任意値を含まないことになるため、評価値は「１」である。
【００６７】
このとき、「ｇ３」の評価値（Ｘ，Ｙ）の「Ｘ」は、「ｇ３」から呼び出される下位関数「ｕｎｄｅｔ」が任意値を返すため、「０」となる。また、「Ｙ」は、下位関数「ｕｎｄｅｔ」の評価値が「０」であるため、「０」となる。
【００６８】
「ｇ２」の評価値（Ｘ，Ｙ）の「Ｘ」は、「ｇ２」から呼び出される下位関数「ｇ３」が任意値を返すため、「０」となる。また、「Ｙ」は、下位関数「ｇ３」の評価値が「０」であるため、「０」となる。
【００６９】
「ｇ１」の評価値（Ｘ，Ｙ）の「Ｘ」は、「ｇ１」から呼び出される下位関数「ｇ２」が任意値を返すため、「０」となる。また、「Ｙ」は、下位関数「ｇ２」の評価値が「０」であるため、「０」となる。
【００７０】
「ｇ５」，「ｇ６」は、下位関数を持たないため、評価値（Ｘ，Ｙ）の「Ｘ」と「Ｙ」は、同じく「１」となる。
【００７１】
「ｇ４」の評価値（Ｘ，Ｙ）の「Ｘ」は、「ｇ４」から呼び出される下位関数「ｇ５」が、「ｇ４」から呼び出される時点では任意値であるため、「０」となる。また、「Ｙ」は、下位関数「ｇ５」の評価値が「１」であるため、「１」となる。
【００７２】
従って、「ｇ１」，「ｇ２」，「ｇ３」，「ｇ４」，「ｇ５」，「ｇ６」の評価値は、それぞれ（０，０），（０，０），（０，０），（０，１），（１，１），（１，１）となる。
【００７３】
この結果を図示したのが図７である。
【００７４】
図７におけるブロック数は、図５と同様に、例として付与した値である。
【００７５】
図７において、“「ｇ１」（０，０）：１８”は、関数「ｇ１」のブロック数は「１８」であり、評価値は（０，０）であることを意味する。同様に、“「ｇ２」（０，０）：２８”は、関数「ｇ２」のブロック数は「２８」であり、評価値は（０，０）であることを意味する。“「ｇ３」（０，０）：１８”は、関数「ｇ３」のブロック数は「１８」であり、評価値は（０，０）であることを意味する。“「ｇ４」（０，１）：２８”は、関数「ｇ４」のブロック数は「２８」であり、評価値は（０，１）であることを意味する。“「ｇ５」（１，１）：１８”は、関数「ｇ５」のブロック数は「１８」であり、評価値は（１，１）であることを意味する。“「ｇ６」（１，１）：３８”は、関数「ｇ６」のブロック数は「３８」であり、評価値は（１，１）であることを意味する。
【００７６】
同様に、図８で「ｅｎｔｒｙ３」がエントリ関数とすると、図９に図示した評価値となる。図９においてもブロック数は、後述する検証対象関数選択部３３の動作を説明するために付与した例である。
【００７７】
図８で、「ｅｎｔｒｙ３」がエントリ関数とする。「ｅｎｔｒｙ３」からは「ｈ１」，「ｈ４」，「ｈ６」の各関数が呼ばれている。
【００７８】
「ｈ１」，「ｈ２」，「ｈ４」は、下位関数を持つ。「ｈ３」，「ｈ５」，「ｈ６」は、下位関数を持たない
【００７９】
ここで、「ｈ３」は、２つの大域変数に値が代入されており、その代入する計算式の中に直接又は間接に任意値を含まないため、図３の規則３により、評価値はそれぞれ「２」となる。「ｈ３」は、下位関数を持たないため、評価値（Ｘ，Ｙ）の「Ｘ」と「Ｙ」は、同じく「２」となる。
【００８０】
「ｈ２」の評価値（Ｘ，Ｙ）の「Ｘ」は、「ｈ２」から呼び出される下位関数「ｈ３」が、「ｈ２」から呼び出される時点では任意値であるため、「０」となる。また、「Ｙ」は、下位関数「ｈ３」の評価値が「２」であるため、「２」となる。
【００８１】
「ｈ１」の評価値（Ｘ，Ｙ）の「Ｘ」は、「ｈ１」から呼び出される下位関数「ｈ２」が、「ｈ１」から呼び出される時点では任意値であるため、「０」となる。また、「Ｙ」は、下位関数「ｈ２」の評価値が「２」であるため、「２」となる。
【００８２】
「ｈ５」，「ｈ６」は、１つの大域変数に値が代入されており、その代入する計算式の中に直接又は間接に任意値を含まないため、図３の規則３により、評価値はそれぞれ「１」となる。「ｈ５」，「ｈ６」は、下位関数を持たないため、評価値（Ｘ，Ｙ）の「Ｘ」と「Ｙ」は、同じく「１」となる。
【００８３】
「ｈ４」の評価値（Ｘ，Ｙ）の「Ｘ」は、「ｈ４」から呼び出される下位関数「ｈ５」が、「ｈ４」から呼び出される時点では任意値であるため、「０」となる。また、「Ｙ」は、下位関数「ｈ５」の評価値が「１」であるため、「１」となる。
【００８４】
従って、「ｈ１」，「ｈ２」，「ｈ３」，「ｈ４」，「ｈ５」，「ｈ６」の評価値は、それぞれ（０，２），（０，２），（２，２），（０，１），（１，１），（１，１）となる。
【００８５】
この結果を図示したのが図９である。
【００８６】
図９におけるブロック数は、図５、図７と同様に、例として付与した値である。
【００８７】
図９において、“「ｈ１」（０，２）：６０”は、関数「ｈ１」のブロック数は「６０」であり、評価値は（０，２）であることを意味する。同様に、“「ｈ２」（０，２）：２８”は、関数「ｈ２」のブロック数は「２８」であり、評価値は（０，２）であることを意味する。“「ｈ３」（２，２）：１８”は、関数「ｈ３」のブロック数は「１８」であり、評価値は（２，２）であることを意味する。“「ｈ４」（０，１）：２８”は、関数「ｈ４」のブロック数は「２８」であり、評価値は（０，１）であることを意味する。“「ｈ５」（１，１）：１８”は、関数「ｈ５」のブロック数は「１８」であり、評価値は（１，１）であることを意味する。“「ｈ６」（１，１）：３８”は、関数「ｈ６」のブロック数は「３８」であり、評価値は（１，１）であることを意味する。
【００８８】
＜検証対象関数選択部３３の動作の説明＞
次に、図１０のフローチャートを参照して、検証対象関数選択部３３が、算出された関数のブロック数と評価値を用いて、検証対象に追加する関数を選択する際の動作（図２のステップＡ４）に関して、詳細に説明する。
【００８９】
すなわち、図２のステップＡ４は、図１０のフローチャートのステップＡ４０１からＡ４１０までの処理を含む。これらのステップに関しては、先に説明した関数の指標値と同様に、モデル検査実行部１３の特性により異なるロジックを適用する必要があるため、その特性に合わせて選択方法を定義する。ここでは、図５と図１１、図７と図１２、及び図９と図１３を参照して、選択方法の例を用いて検証対象関数選択部３３の動作を具体的に説明する。
【００９０】
図１０のフローチャートにおいて、判断済マークというのは、ＣＦＧにおける各関数のモデルに対して設定されるフラグ情報であり、処理の過程で判断済マークをつけることで、その関数のモデルを検査対象に含める／含めないの判断が既に設定済みであることを示している。
【００９１】
＜（ａ）図５及び図１１の例に対する動作＞
まず、図５及び図１１の例に対する検証対象関数選択部３３の動作を説明する。この例では、評価値が高い、すなわち上位関数に対する影響度が高い順番に、関数が選択されることを説明する。また、検査仕様１で最大ブロック数には「７０」が指定されているものとする。
【００９２】
（１）ステップＡ４０１
検証対象関数選択部３３は、判断済マークがついていない関数の中で、エントリ関数からの呼び出し階層の最も低い関数群を選ぶ。この段階では、判断済マークがついている関数はない。検証対象関数選択部３３は、エントリ関数からの呼び出し階層が全て同じなので、「ｆ１」，「ｆ２」，「ｆ３」を選ぶ。
【００９３】
（２）ステップＡ４０２
検証対象関数選択部３３は、関数候補があるか確認する。すなわち、検証対象関数選択部３３は、選ばれた関数群があるか確認する。ここでは、選ばれた「ｆ１」，「ｆ２」，「ｆ３」が関数候補となる。検証対象関数選択部３３は、関数候補（選ばれた関数群）がなければ、ここで処理を終了する。
【００９４】
（３）ステップＡ４０３
検証対象関数選択部３３は、関数候補（選ばれた関数群）があれば、選ばれた関数群のうち呼び出し階層が同位のものの中で、評価値（Ｘ，Ｙ）の「Ｘ」の値が最大の関数群を選ぶ。ここでは、検証対象関数選択部３３は、選ばれた「ｆ１」，「ｆ２」，「ｆ３」の中で、評価値「Ｘ」が最大なものは「ｆ３」なので、「ｆ３」を選ぶ。
【００９５】
（４）ステップＡ４０４
次に、検証対象関数選択部３３は、評価値（Ｘ，Ｙ）の「Ｘ」の値が同位のものの中で、評価値（Ｘ，Ｙ）の「Ｙ」の値が最大の関数群を選ぶ。
【００９６】
（５）ステップＡ４０５
次に、検証対象関数選択部３３は、評価値（Ｘ，Ｙ）の「Ｙ」の値が同位のものの中で、関数のブロック数が最小の関数群を選ぶ。
【００９７】
（６）ステップＡ４０６
次に、検証対象関数選択部３３は、関数のブロック数が同位のものの中で、ＣＦＧモデル上で最左の関数を選ぶ。
【００９８】
この例では、ステップＡ４０３の段階で一つの関数「ｆ３」に絞りこまれたので、ステップＡ４０４からステップＡ４０６を適用しても、「ｆ３」が選ばれることになる。
【００９９】
（７）ステップＡ４０７
次に、検証対象関数選択部３３は、選択された関数の評価値（Ｘ，Ｙ）の「Ｙ」の値が「０」でないか確認する。ここでは、選ばれた「ｆ３」の評価値（Ｘ，Ｙ）の「Ｙ」は「０」でないので、次の処理（ステップＡ４０８）に移る。
【０１００】
（８）ステップＡ４０８
次に、検証対象関数選択部３３は、累積ブロック数に関数ブロック数を加算した値が検査仕様１で与えられている最大ブロック数を超えないか確認する。ここでは、この段階での累積ブロック数は「０」であり、この累積ブロック数に「ｆ３」のブロック数「３８」を加算した値「３８」は、この例で仮定した最大ブロック数「７０」を超えないので、次の処理（ステップＡ４０９）に移る。
【０１０１】
（９）ステップＡ４０９
次に、検証対象関数選択部３３は、該当関数を検証対象に追加し、判断済マークを付ける。また、検証対象関数選択部３３は、累積ブロック数に該当関数のブロック数を加算する。ここでは、検証対象関数選択部３３は、ここまでの条件を満たした「ｆ３」を検査対象に追加し、判断済マークを付ける。累積ブロック数は「３８」となる。その後、最初の処理（ステップＡ４０１）に戻る。
【０１０２】
検証対象関数選択部３３は、再び、ステップＡ４０１からステップＡ４０７を、この段階で判断済マークがついていない「ｆ１」，「ｆ２」に適用し、「ｆ２」を選択する。この処理の流れを以下に詳述する。
【０１０３】
（１０）ステップＡ４０１
検証対象関数選択部３３は、判断済マークがついていない関数の中で、エントリ関数からの呼び出し階層の最も低い関数群を選ぶ。検証対象関数選択部３３は、この段階で、「ｆ３」に判断済マークがついているので、「ｆ１」，「ｆ２」を選ぶ。
【０１０４】
（１１）ステップＡ４０２
検証対象関数選択部３３は、関数候補があるか確認する。すなわち、検証対象関数選択部３３は、選ばれた関数群があるか確認する。ここでは、選ばれた「ｆ１」，「ｆ２」が関数候補となる。検証対象関数選択部３３は、関数候補（選ばれた関数群）がなければ、ここで処理を終了する。
【０１０５】
（１２）ステップＡ４０３
検証対象関数選択部３３は、関数候補（選ばれた関数群）があれば、選ばれた関数群のうち呼び出し階層が同位のものの中で、評価値（Ｘ，Ｙ）の「Ｘ」の値が最大の関数群を選ぶ。ここでは、検証対象関数選択部３３は、選ばれた「ｆ１」，「ｆ２」の中で、評価値「Ｘ」が最大なものは「ｆ２」なので、「ｆ２」を選ぶ。
【０１０６】
（１３）ステップＡ４０４
次に、検証対象関数選択部３３は、評価値（Ｘ，Ｙ）の「Ｘ」の値が同位のものの中で、評価値（Ｘ，Ｙ）の「Ｙ」の値が最大の関数群を選ぶ。
【０１０７】
（１４）ステップＡ４０５
次に、検証対象関数選択部３３は、評価値（Ｘ，Ｙ）の「Ｙ」の値が同位のものの中で、関数のブロック数が最小の関数群を選ぶ。
【０１０８】
（１５）ステップＡ４０６
次に、検証対象関数選択部３３は、関数のブロック数が同位のものの中で、ＣＦＧモデル上で最左の関数を選ぶ。
【０１０９】
この例では、ステップＡ４０３の段階で一つの関数「ｆ２」に絞りこまれたので、ステップＡ４０４からステップＡ４０６を適用しても、「ｆ２」が選ばれることになる。
【０１１０】
（１６）ステップＡ４０７
次に、検証対象関数選択部３３は、選択された関数の評価値（Ｘ，Ｙ）の「Ｙ」の値が「０」でないか確認する。ここでは、選ばれた「ｆ２」の評価値（Ｘ，Ｙ）の「Ｙ」は「０」でないので、次の処理（ステップＡ４０８）に移る。
【０１１１】
（１７）ステップＡ４０８
次に、検証対象関数選択部３３は、累積ブロック数に関数ブロック数を加算した値が検査仕様１で与えられている最大ブロック数を超えないか確認する。ここでは、この段階での累積ブロック数は「３８」であり、「ｆ２」のブロック数「２８」を加算した値「６６」は、この例で設定された最大ブロック数「７０」を超えないので、次の処理（ステップＡ４０９）に移る。
【０１１２】
（１８）ステップＡ４０９
次に、検証対象関数選択部３３は、該当関数を検証対象に追加し、判断済マークを付ける。また、検証対象関数選択部３３は、累積ブロック数に該当関数のブロック数を加算する。ここでは、検証対象関数選択部３３は、ここまでの条件を満たした「ｆ２」を検査対象に追加し、判断済マークを付ける。累積ブロック数は「６６」となる。その後、最初の処理（ステップＡ４０１）に戻る。
【０１１３】
検証対象関数選択部３３は、再び、ステップＡ４０１〜Ａ４０７を、この段階で判断済マークがついていない「ｆ１」に適用することになる。この処理の流れを以下に詳述する。
【０１１４】
（１９）ステップＡ４０１
検証対象関数選択部３３は、判断済マークがついていない関数の中で、エントリ関数からの呼び出し階層の最も低い関数群を選ぶ。検証対象関数選択部３３は、この段階で、「ｆ２」，「ｆ３」に判断済マークがついているので、「ｆ１」を選ぶ。
【０１１５】
（２０）ステップＡ４０２
検証対象関数選択部３３は、関数候補があるか確認する。すなわち、検証対象関数選択部３３は、選ばれた関数群があるか確認する。ここでは、選ばれた「ｆ１」が関数候補となる。検証対象関数選択部３３は、関数候補（選ばれた関数群）がなければ、ここで処理を終了する。
【０１１６】
（２１）ステップＡ４０３
検証対象関数選択部３３は、関数候補（選ばれた関数群）があれば、選ばれた関数群のうち呼び出し階層が同位のものの中で、評価値（Ｘ，Ｙ）の「Ｘ」の値が最大の関数群を選ぶ。ここでは、選ばれた関数が「ｆ１」しかないため、「ｆ１」が選ばれることになる。
【０１１７】
（２２）ステップＡ４０４
次に、検証対象関数選択部３３は、評価値（Ｘ，Ｙ）の「Ｘ」の値が同位のものの中で、評価値（Ｘ，Ｙ）の「Ｙ」の値が最大の関数群を選ぶ。
【０１１８】
（２３）ステップＡ４０５
次に、検証対象関数選択部３３は、評価値（Ｘ，Ｙ）の「Ｙ」の値が同位のものの中で、関数のブロック数が最小の関数群を選ぶ。
【０１１９】
（２４）ステップＡ４０６
次に、検証対象関数選択部３３は、関数のブロック数が同位のものの中で、ＣＦＧモデル上で最左の関数を選ぶ。
【０１２０】
この例では、ステップＡ４０３の段階で一つの関数「ｆ１」に絞りこまれたので、ステップＡ４０４からステップＡ４０６を適用しても、「ｆ１」が選ばれることになる。
【０１２１】
（２５）ステップＡ４０７
次に、検証対象関数選択部３３は、選択された関数の評価値（Ｘ，Ｙ）の「Ｙ」の値が「０」でないか確認する。ここでは、選ばれた「ｆ１」の評価値（Ｘ，Ｙ）の「Ｙ」は「０」でないので、次の処理（ステップＡ４０８）に移る。
【０１２２】
（２６）ステップＡ４０８
次に、検証対象関数選択部３３は、累積ブロック数に関数ブロック数を加算した値が検査仕様１で与えられている最大ブロック数を超えないか確認する。ここでは、この段階での累積ブロック数は「６６」であり、「ｆ１」のブロック数「１８」を加算すると、仮定した最大ブロック数「７０」を超えるため、仮定した最大ブロック数を超えない場合とは異なる処理（ステップＡ４１０）に移る。
【０１２３】
（２７）ステップＡ４１０
次に、検証対象関数選択部３３は、該当関数及び下位関数に判断済マークを付ける。ここでは、検証対象関数選択部３３は、「ｆ１」に判断済マークを付ける。その後、最初の処理（ステップＡ４０１）に戻る。
【０１２４】
検証対象関数選択部３３は、再び、ステップＡ４０１を適用するが、この段階で判断済マークがついていない関数が存在しないため、ステップＡ４の処理を終了する。
【０１２５】
このようにして、「ｆ３」，「ｆ２」の順番に関数が選択される。「ｆ３」が「ｅｎｔｒｙ１」に与える影響は「大域変数３個分」であり、「ｆ２」が「ｅｎｔｒｙ１」に与える影響は「アドレス渡し引数２個分」であり、影響度の高いものが順番に選択されることがわかる。
【０１２６】
これを図示したのが図１１である。図１１で丸付数字は選択された順番を示し、星印は選択されなかった関数を示す。その他は図５と同じである。
【０１２７】
図１１において、“「ｆ１」（１，１）：１８”は、関数「ｆ１」のブロック数は「１８」であり、評価値は（１，１）であることを意味する。同様に、“「ｆ２」（２，２）：２８”は、関数「ｆ２」のブロック数は「２８」であり、評価値は（２，２）であることを意味する。“「ｆ３」（３，３）：３８”は、関数「ｆ３」のブロック数は「３８」であり、評価値は（３，３）であることを意味する。
【０１２８】
＜（ｂ）図７及び図１２の例に対する動作＞
次に、図７及び図１２の例に対する検証対象関数選択部３３の動作を説明する。この例では、任意値を計算式中に含む関数が選択されないことを説明する。また、検査仕様１で最大ブロック数には「９０」が指定されているものとする。
【０１２９】
図５に対する処理と同様に、図７に対して、ステップＡ４０１〜Ａ４０９を繰り返し適用することにより、「ｇ１」，「ｇ４」，「ｇ６」の中から、「ｇ６」、「ｇ４」の順に検証対象として選択されるが、その後、「ｇ１」に対してステップＡ４０７を適用すると、「ｇ１」の評価値（Ｘ，Ｙ）の「Ｙ」が「０」なので、「ｇ１」は検証対象とはみなされない。
【０１３０】
更に、ステップＡ４１０によって、「ｇ１」及びその下位関数「ｇ２」，「ｇ３」も同様に検証対象とはみなされないまま、判断済マークが付けられる。その後、ステップＡ４０１に戻り、「ｇ５」が検証対象に追加された時点で、ステップＡ４の処理は終了する。
【０１３１】
このようにして、「ｇ６」，「ｇ４」，「ｇ５」の順番に関数が選択される。任意値を含む「ｇ１」，「ｇ２」，「ｇ３」が検証対象にならなかったことがわかる。
【０１３２】
これを図示したのが図１２である。図１２で丸付数字は選択された順番を示し、星印は選択されなかった関数を示す。その他は図７と同じである。
【０１３３】
図１２において、“「ｇ１」（０，０）：１８”は、関数「ｇ１」のブロック数は「１８」であり、評価値は（０，０）であることを意味する。同様に、“「ｇ２」（０，０）：２８”は、関数「ｇ２」のブロック数は「２８」であり、評価値は（０，０）であることを意味する。“「ｇ３」（０，０）：１８”は、関数「ｇ３」のブロック数は「１８」であり、評価値は（０，０）であることを意味する。“「ｇ４」（０，１）：２８”は、関数「ｇ４」のブロック数は「２８」であり、評価値は（０，１）であることを意味する。“「ｇ５」（１，１）：１８”は、関数「ｇ５」のブロック数は「１８」であり、評価値は（１，１）であることを意味する。“「ｇ６」（１，１）：３８”は、関数「ｇ６」のブロック数は「３８」であり、評価値は（１，１）であることを意味する。
【０１３４】
＜（ｃ）図９及び図１３の例に対する動作＞
次に、図９及び図１３の例に対する検証対象関数選択部３３の動作を説明する。この例では、最大ブロック数制限を超える関数が選択されないことを説明する。また、検査仕様１で最大ブロック数には「９０」が指定されているものとする。
【０１３５】
この場合も、図５、図７と同様に、図９に対してステップＡ４０１〜Ａ４０９の一連の処理を繰り返し適用する。
【０１３６】
まず、「ｈ６」が対象関数として選択された後に、「ｈ１」がステップＡ４０４で選ばれるが、この場合は、その後にＡ４０８を適用する時点で、この段階での累積ブロック数３８に対して、「ｈ１」のブロック数「６０」を加算した値は、指定された最大ブロック数「９０」を超えるため、検証対象の選択からはずれる。
【０１３７】
更に、ステップＡ４１０において、その下位関数「ｈ２」、「ｈ３」と共に判断済マークが付けられる。
【０１３８】
この後、残った「ｈ４」、「ｈ５」に対してステップＡ４０１〜Ａ４０９が適用されるが、「ｈ４」、「ｈ５」は最大ブロック数制限を越えることがないので、検証対象に追加され、判断済マークが付く。この時点で関数候補がなくなり、ステップＡ４の処理は終了する。
【０１３９】
このようにして、「ｈ６」，「ｈ４」，「ｈ５」の順番に関数が選択される。「ｈ１」は最大ブロック数制限を超えるため、検証対象にならない。
【０１４０】
これを図示したのが図１３である。図１３で丸付数字は選択された順番を示し、星印は選択されなかった関数を示す。その他は図９と同じである。
【０１４１】
図１３において、“「ｈ１」（０，２）：６０”は、関数「ｈ１」のブロック数は「６０」であり、評価値は（０，２）であることを意味する。同様に、“「ｈ２」（０，２）：２８”は、関数「ｈ２」のブロック数は「２８」であり、評価値は（０，２）であることを意味する。“「ｈ３」（２，２）：１８”は、関数「ｈ３」のブロック数は「１８」であり、評価値は（２，２）であることを意味する。“「ｈ４」（０，１）：２８”は、関数「ｈ４」のブロック数は「２８」であり、評価値は（０，１）であることを意味する。“「ｈ５」（１，１）：１８”は、関数「ｈ５」のブロック数は「１８」であり、評価値は（１，１）であることを意味する。“「ｈ６」（１，１）：３８”は、関数「ｈ６」のブロック数は「３８」であり、評価値は（１，１）であることを意味する。
【０１４２】
本発明の効果は、モデル検査に先立って、検証対象のモデルの再構築を行うことにより、与えられた検証時間内により有効な検証結果が得られることである。その理由は、検証対象関数選択手段により、エントリ関数から呼び出される関数のうち、モデルの状態数が大きいために規定時間内では検証結果が得られない可能性が高い関数をモデル化対象からはずすことで、比較的短い時間で検証が可能なその他の関数の検証に、より多くの検証時間の配分が可能となるためである。
【０１４３】
以上のように、本発明は、モデル検査技法を利用してソースコードの検証を行う処理系において、検証対象の起点となる関数及び検証可能な最大ブロック数を指定することにより、検証効果が高くなる関数を自動選択する機構を有する装置及び方法に関する。
【０１４４】
本発明では、モデルの状態数を増やす最も大きな要素として、任意値をとる変数や関数の返却値に着目する。
【０１４５】
任意値は、与えられた条件のもとで特定の値あるいはある限られた範囲の値をとることが決定できないことを意味している。
【０１４６】
また、任意値とみなされる変数や関数の参照に対しては、あらゆる値を取る可能性があるものとしてモデル化する必要があるため、モデル検査における計算量が非常に大きくなり、上限時間内に検証結果が得られない可能性が非常に高い。
【０１４７】
更に、もう一つの着目点として、ＣＦＧモデルにおけるブロック数の上限値を考慮する。一般に、検証対象となるモデルのＣＦＧ表現を構成する全体ブロック数と検証時間との間には相関があり、ブロック数が多くなればなるほど検証時間が長くなる。
【０１４８】
本発明では、モデル検査を実行する前に、上記の２つの要素を利用して、検証対象のモデルの再構築を行うことにより、与えられた検証時間内により有効な検証結果が得られるモデルを出力する。
【０１４９】
まず、与えられたソースコードから変換されたＣＦＧモデルにおいて、任意値を取る変数や関数の参照を含む一連の関数呼び出しフローを検査対象から除外する。
【０１５０】
更に、呼び出し上位の関数に対して、下位の関数がどれだけ多くのコンテキストを与えているか、つまり下位関数をモデル化することで、どれだけ上位関数の検証精度が高くなるかという基準で、ランク付けを行った上で、再構築するモデルの全体ブロック数が、事前に指定された上限の範囲内に収まるように関数の取捨選択を行う。
【０１５１】
ここで「コンテキスト」とは、上位関数が使用する変数に対して下位関数が値を代入することである。上位関数が使用する変数に対して下位関数が値を代入するには、戻り値を利用する、アドレス渡し引数を利用する、大域変数を利用するの３つの方法がある。
【０１５２】
このようなモデル再構築手法により、与えられた検証時間を効果的に利用することが可能となり、より多くの検証結果を得ることが可能となる。
【０１５３】
本発明の検証対象関数自動選択装置は、検査仕様と、検査対象コードと、検査結果と、モデル検査制御手段と、記憶手段と、検証対象関数選択手段を含む。
【０１５４】
ここで、モデル検査制御手段は、コンパイラ最適化処理及び計算木論理（ＣＴＬ）を用いた記号モデル検査法等の従来技術で構成する。
【０１５５】
モデル検査制御手段は、ＣＦＧモデル作成手段と、検査モデル作成手段と、モデル検査実行手段と、検査結果出力手段を含む。
【０１５６】
記憶手段は、変換前ＣＦＧモデル記憶手段と、変換後ＣＦＧモデル記憶手段と、検査モデル記憶手段を含む。
【０１５７】
検証対象関数選択手段は、呼び出し関数検出手段と、関数評価手段と、検証対象関数追加手段と、ＣＦＧモデル変換手段を含む。
【０１５８】
本発明によれば、モデル検査を利用したソースコード検証の検証効果を高める用途に適用できる。
【０１５９】
以上、本発明の実施形態を詳述してきたが、実際には、上記の実施形態に限られるものではなく、本発明の要旨を逸脱しない範囲の変更があっても本発明に含まれる。
【符号の説明】
【０１６０】
１…  検査仕様
２…  検査対象コード
３…  検査結果
１０…  モデル検査制御部
１１…  ＣＦＧモデル作成部
１２…  検査モデル作成部
１３…  モデル検査実行部
１４…  検査結果出力部
２０…  記憶装置
２１…  変換前ＣＦＧモデル記憶部
２２…  変換後ＣＦＧモデル記憶部
２３…  検査モデル記憶部
３０…  検証対象関数選択部
３１…  呼び出し関数検出部
３２…  関数評価部
３３…  検証対象関数追加部
３４…  ＣＦＧモデル変換部
【図１】
2010211521.tif 000003
【図２】
2010211521.tif 000004
【図３】
2010211521.tif 000005
【図４】
2010211521.tif 000006
【図５】
2010211521.tif 000007
【図６】
2010211521.tif 000008
【図７】
2010211521.tif 000009
【図８】
2010211521.tif 000010
【図９】
2010211521.tif 000011
【図１０】
2010211521.tif 000012
【図１１】
2010211521.tif 000013
【図１２】
2010211521.tif 000014
【図１３】
2010211521.tif 000015