(57)【要約】【課題】ＳＡＴ手法を応用してゴールデンを解析することにより、動作要件を満たすテスト制約を自動抽出するできるようにする。【解決手段】ゴールデンを入力し、入力されたゴールデンの所定機能毎にＣＦＧを生成し、制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成し、前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、ゴールデンの制御条件の全体を表す論理関数を構成し、ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求め、論理関数の充足解が存在するとき該充足解をテスト制約の一例として表示し、得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す。【選択図】図１
2010238057.tif 000002
【特許請求の範囲】
【請求項１】
所望の仕様を満たすゴールデンの制御条件からテスト制約を抽出するテスト制約抽出装置において、
対象となるゴールデンの所定機能毎に制御構造を生成する制御構造生成手段と、
前記制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成する制御経路分析手段と、
前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、前記制御条件の全体を表す論理関数を構成する論理関数構成手段と、
ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求める充足可能性判定手段と、
得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す別解探索・記憶手段と、
前記各手段の制御を行う制御手段と、
を備えることを特徴とするテスト制約抽出装置。
【請求項２】
所望の仕様を満たすゴールデンの制御条件からテスト制約を抽出するテスト制約抽出方法において、
対象となるゴールデンの所定機能毎に制御構造を生成する制御構造生成ステップと、
前記制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成する制御経路分析ステップと、
前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、前記制御条件の全体を表す論理関数を構成する論理関数構成ステップと、
ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求める充足可能性判定ステップと、
得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す別解探索・記憶ステップと、
を備えることを特徴とするテスト制約抽出方法。
【請求項３】
所望の仕様を満たすゴールデンの制御条件からテスト制約を抽出するテスト制約抽出プログラムにおいて、
対象となるゴールデンの所定機能毎に制御構造を生成する制御構造生成ステップと、
前記制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成する制御経路分析ステップと、
前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、前記制御条件の全体を表す論理関数を構成する論理関数構成ステップと、
ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求める充足可能性判定ステップと、
得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す別解探索・記憶ステップと、
を備えることを特徴とするテスト制約抽出プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、機能検証に用いるテスト制約を自動抽出する装置、方法およびプログラムに関するものである。
【背景技術】
【０００２】
あるシステムを実現するための要求条件（仕様Ｓ）があり、その機能を実現するソフトウェア（実装Ｄ１）があり、さらに、高性能化などの理由のために、同等の機能をＬＳＩ等のハードウェア（実装Ｄ２）で実現する場合を考える。このとき、機能検証とは、実装したシステムが、その仕様に計画された所望の動作と完全一致することを保証することである。機能検証は、大きく分けて２つのアプローチがある。
【０００３】
１つはフォーマル検証と呼ばれる方法である。これは機能検証の問題を数学的な証明問題に帰着することにより解決を図る。産業的に広く浸透しているとは言いがたいが、技術的には十分実用レベルに達しているものが出ている。特に、論理関数の充足可能性判定問題を解くＳＡＴ手法は、フォーマル検証の中核エンジンとして定着していて、例えばソフトウェアの静的解析技術への応用が挙げられる（非特許文献１参照）。これは実装Ｄ１の検証を対象としたもので、ソフトウェアが一般的に満たすべき性質の検証問題をＳＡＴ手法により効率的に解決する。
【０００４】
一方、従来から広く行われている方法にシミュレーションがある。仕様Ｓの要件を完全に満たす実装Ｄ１があると仮定したとき、実装Ｄ１のプログラムをゴールデンと呼ぶ。実装Ｄ２が機能的に正しく実現されているかどうかを調べる場合、通常はテストパタンをゴールデンと実装Ｄ２に入力し、シミュレーションによって双方の出力の一致を確認する。このとき、ゴールデンは、実装Ｄ２が正しく実現できているかどうかを判断するためのリファレンス・プログラムとして動作している。一致検証を行うためには、テストベンチと呼ばれる周辺モジュールが必要になる。
【発明の概要】
【発明が解決しようとする課題】
【０００５】
思いつく限りの検証項目をシミュレーションする場合、検証者が仕様を熟知していれば、ピンポイントで動作確認ができるので効果的である。しかし、テストベンチとテストパタンの作成工数が問題となる。また、検証を行う上で前提となる複雑なテスト制約を仕様Ｓから洗い出す必要があるが、必ずしも仕様や設計の意図を完全には知りえない第三者が、動作要件を満たすテスト制約を作成することは容易ではない。さらに、テスト制約やテスト制約に基づくテストパタンを可能な限り多く作成するのは困難な作業である。
【０００６】
本発明の目的は、ＳＡＴ手法を応用してゴールデンを解析することにより、動作要件を満たすテスト制約を自動抽出するできるようにすることにある。
【課題を解決するための手段】
【０００７】
上記目的を達成するために、請求項１にかかる発明は、所望の仕様を満たすゴールデンの制御条件からテスト制約を抽出するテスト制約抽出装置において、対象となるゴールデンの所定機能毎に制御構造を生成する制御構造生成手段と、前記制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成する制御経路分析手段と、前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、前記制御条件の全体を表す論理関数を構成する論理関数構成手段と、ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求める充足可能性判定手段と、得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す別解探索・記憶手段と、前記各手段の制御を行う制御手段と、備えることを特徴とする。
【０００８】
請求項２にかかる発明は、所望の仕様を満たすゴールデンの制御条件からテスト制約を抽出するテスト制約抽出方法において、対象となるゴールデンの所定機能毎に制御構造を生成する制御構造生成ステップと、前記制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成する制御経路分析ステップと、前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、前記制御条件の全体を表す論理関数を構成する論理関数構成ステップと、ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求める充足可能性判定ステップと、得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す別解探索・記憶ステップと、を備えることを特徴とする。
【０００９】
請求項３にかかる発明は、所望の仕様を満たすゴールデンの制御条件からテスト制約を抽出するテスト制約抽出プログラムにおいて、対象となるゴールデンの所定機能毎に制御構造を生成する制御構造生成ステップと、前記制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成する制御経路分析ステップと、前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、前記制御条件の全体を表す論理関数を構成する論理関数構成ステップと、ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求める充足可能性判定ステップと、得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す別解探索・記憶ステップと、を備えることを特徴とする。
【発明の効果】
【００１０】
本発明によれば、ＳＡＴ手法を応用してゴールデンを解析することにより、機能検証を行う際に、検証目的に合致するテスト制約を複数組自動抽出することができるので、複雑に入り組んだテスト制約の作成にかかる負担を軽減できる。また、必ずしも仕様を熟知していなくてもテスト制約を抽出することができるので、仕様を理解するための工数を減らすことが期待できる。抽出したテスト制約は、ソフトウェアのテストだけでなく、ハードウェアの機能検証にも用いることができる。さらに、本発明が抽出したテスト制約は、テスト・シーケンスの作成にも活用することができるため、テストパタン作成にかかる工数を削減できる可能性がある。これらの効果により検証生産性が向上し、シミュレーション環境構築に要するトータルの検証期間の短縮を図ることができる。
【図面の簡単な説明】
【００１１】
【図１】本発明のテスト制約抽出方法を実施するシステムのブロック図である。
【図２】図１の制御装置８の動作手順を示すフローチャートである。
【図３】機能１の制御条件に着目した状態を示す図である。
【図４】機能１の制御条件を論理式で表現した図である。
【図５】機能２の制御条件に着目した状態を示す図である。
【図６】機能２の制御条件を論理式で表現した図である。
【図７】機能１と機能２の論理式から論理関数Ｆを構成する例を示す図である。
【図８】論理関数Ｆの充足解と、充足解を複数抽出する手順を示す図である。
【発明を実施するための形態】
【００１２】
次に、本発明の実施例について図面を参照して説明する。図１は本発明のテスト制約抽出方法を実施するシステム（装置）のブロック図である。本装置は、ゴールデン（プログラム）を入力する入力装置１と、入力されたゴールデンの所定機能毎に制御構造（後記するＣＦＧ）を生成する制御構造生成装置２と、前記制御構造から目標に到達する分岐ノードのみを抽出した前記所定機能毎の制御経路を分析生成する制御経路分析装置３と、前記所定機能毎に前記制御経路を表す論理式を生成し、得られた各論理式を組み合わせて、ゴールデンの制御条件の全体を表す論理関数を構成する論理関数構成装置４と、ＳＡＴ手法を用いて前記論理関数の全体の値を充足する充足解を求める充足可能性判定器５と、論理関数の充足解が存在するとき該充足解をテスト制約の一例として表示する出力装置６と、得られた前記充足解をテスト制約として記憶するとともに、該充足解の論理否定と元の論理関数との論理積を演算し、別のテスト制約の探索を繰り返す別解探索・記憶装置７と、全体の制御を制御プログラムによって制御するコンピュータによる制御装置８と、信号線９とで構成される。このように、本システムによる処理は、コンピュータと制御プログラムによって実現でき、制御プログラムを記録媒体に記録することも、ネットワークを通して提供することも可能である。
【００１３】
図２は、図１の制御装置８の動作手順を示すフローチャートである。以下では、ステップＳ１〜Ｓ４を処理前半部とし、ステップＳ５〜Ｓ９を処理後半部として説明する。
【００１４】
＜処理前半部＞
まず、ステップＳ１では、入力装置１からゴールデンを図１のテスト制約抽出システムに入力する。制御構造生成装置２はゴールデンを入力として、制御フローグラフ（以下ＣＦＧ）を生成する。図３では、ゴールデンを構成する一関数の制御構造（以下機能１）のプログラムを(a)に、該機能１の関数から自動生成したＣＦＧを(b)に示した。ＣＦＧの自動生成には、プログラム・フロントエンドとして広く知られているものを用いることができる。
【００１５】
次に、ステップＳ２ではＣＦＧの制御ノードの位置を示すポインタ（位置）Ｐｉを定義する。制御ノードとは、プログラムの実行経路の制御情報を表す単位で、図３(b)では番号付きで示されている（ｉ＝９３３〜９４８）。制御ノード同士は一方向の矢印で接続され、制御のベクトルを示す。矢印を制御エッジと呼ぶ。ｉの値が大きいほど、ＣＦＧにおける機能的な位置が深いことを意味する。機能１の関数では、ｉ＝９３３が当該関数の開始ノードを示し、ｉ＝９４８が当該関数の終端ノードを示している。本実施例は、ｉ＝９４７に到達する、すなわち機能１が関数の最終段まで実行し、何らかの計算結果を返すことを機能確認の目標として指定しており、ｉ＝９４８に到達するためのプログラムの実行経路を分析し、テスト制約を抽出するものである。
【００１６】
また、通常、ゴールデンは複数機能の集合体として構成されるため、複数の関数を保持しているが、関数は互いに呼び出し合う等の機能的な依存関係を持っており、それによりゴールデン全体の動作が決まる。図５(a)は図３(b)のｃｏｎｄ４で呼び出される関数の制御構造（以下機能２）のプログラムを示し、図５(b)は該機能２の関数から自動生成したＣＦＧを示す。機能２では、ｉ＝９１２が関数の開始ノードを示し、ｉ＝９３０が終端ノードで機能確認の目標として指定している。
【００１７】
ステップＳ３では、制御経路分析装置３がＣＦＧに基づいて制御経路の分析を行う。図３(b)と図５(b)に、分岐条件を表すＣＦＧの制御ノードに着目した様子を示す。該当する分岐ノードにおいて、条件式ｃｏｎｄの評価値がＴＲＵＥなら左エッジを、ＦＡＬＳＥなら右エッジを示す。図４と図６は、機能１と機能２について、分岐ノードのみ抽出した制御関係を示す有向グラフである。つまり、順次実行文やその他経路の増減に直接関係のないノードを除外し、抽象化したＣＦＧになっている。繰返し制御文については、基本的に同じ順次実行文を繰返すだけであるため、展開したループの中身を１回だけ辿ると考え、抽象化したＣＦＧモデル上では扱わない。
【００１８】
論理関数構成装置４は、ステップＳ４で関数の開始〜終端ノード間の経路情報を、条件式の値ＴＲＵＥ／ＦＡＬＳＥと、論理演算ＡＮＤ（∧）、ＯＲ（∨）、ＮＯＴ（〜）の関係式で記述する。これを論理式Ｅｎとする。具体的には、図４と図６のＣＦＧ各分岐ノードに論理変数を割り当てる。この論理変数をリテラルＬｎとする。リテラルは論理変数の肯定形（Ｌｎ）または否定形（〜Ｌｎ）を表す。図４のリテラルはＬ５＝（ａ、ｂ、ｃ、ｄ、ｅ）、図６のリテラルはＬ７＝（ｍ、ｎ、ｏ、ｐ、ｑ、ｒ、ｓ）と割り当てられている。このとき、図４と図６のＣＦＧはそれぞれ以下の論理式(1)、(2)で表される。
Ｅｆｕｎｃ１＝〜ａ∧〜ｂ∧〜ｃ∧ｄ∧（ｅ∨〜ｅ）                      (1)
Ｅｆｕｎｃ２＝〜ｍ∧〜ｎ∧〜ｏ∧ｐ∧（ｑ∨〜ｑ）∧ｒ∧（ｓ∨〜ｓ）    (2)
【００１９】
すなわち、ノード間の経路が１本であれば各肯定／否定リテラルを項としてＡＮＤでとりまとめ、２本なら肯定リテラルと否定リテラルをＯＲでとりまとめたものを項としてＡＮＤでつなげばよい。このようにすべての関数についてステップＳ３とＳ４の処理を繰り返すことにより、制御経路情報を論理式で表現することができる。
【００２０】
＜処理後半部＞
図２のステップＳ５では、前処理として、ステップＳ４までで得られた論理式Ｅｎからゴールデン全体を構成する論理関数Ｆを作成する。論理関数Ｆの表現形式は、後段の処理の都合上、何らかの規則に従って記述されている方式を採る必要がある。表現形式としては、積和形論理式や和積形論理式のような標準形がある。公知の充足可能性判定器の多くは和積形論理式を受け付けるようになっているが、利用シーンに応じて適切な表現形式を使い分ければよい。本実施例では、式(1)と式(2)に示すように、和積形論理式で表現する。論理関数Ｆの作成例を図７に示す。論理関数Ｆは論理式Ｅｎの論理積で表される。すなわち、本実施例における機能１と機能２の論理式から作成される論理関数Ｆは以下の通りである。
Ｆ＝Ｅｆｕｎｃ１∧Ｅｆｕｎｃ２                                          (3)
【００２１】
ここで、機能２は図３において機能１のｉ＝９４２で呼び出されている。図４によると、ｉ＝９４２ノードには論理変数ｄが割り当てられている。そのため、論理変数ｄは機能２の論理式Ｅｆｕｎｃ２で置き換えることができる。つまり、機能１が機能２を呼び出し、それらの依存関係全体を表現した論理関数Ｆは以下のように記述することができる。
Ｆ＝〜ａ∧〜ｂ∧〜ｃ∧〜ｍ∧〜ｎ∧〜ｏ∧ｐ∧（ｑ∨〜ｑ）∧ｒ∧（ｓ∨〜ｓ）∧        （ｅ∨〜ｅ）                                                    (4)
【００２２】
次にステップＳ７では、式(4)の論理関数Ｆを充足可能性判定器５に与える。充足可能性判定器５には、ＳＡＴ手法を用いた公知の充足可能性判定器を利用することができる。充足可能性判定器５は、論理関数Ｆ全体を１とするような入力論理変数の組合せが存在するか否か判定を行う。そのような論理変数の組が存在する場合には、充足可能（ＳＡＴｉｓｆｉａｂｌｅ）と出力装置６に表示し、反対に、そのような変数の組合せが存在しない場合には、充足不可能（ＵＮＳＡＴｉｓｆｉａｂｌｅ）と出力装置６に表示する。
【００２３】
ステップＳ８で、もしＳＡＴｉｓｆｉａｂｌｅと表示されれば、論理関数Ｆを充足する充足解が存在するので、充足解がひとつ例示される。この充足解がテスト制約ということになる。テスト制約はＴＲＵＥ／ＦＡＬＳＥの組合せで表される制御情報であり、ステップＳ２で指定した機能確認目標に到達することが保証されている。すなわち、ここで得られた制御情報が機能検証の目的を満たすテスト制約そのものを意味する。図８に例を示す。ここでは、充足解Ａ８が表示されたので、充足解Ａ８として別解探索・記憶装置７に保存する。充足可能性判定器５は通常、充足解をひとつしか表示しないため、別の充足解を例示させたい場合は以下のステップＳ９を実施する。
【００２４】
複数の充足解Ａｉが存在するとき、別解を表示させるためには、ステップＳ９で「Ｆ＝Ｆ∧〜Ａｉ」を演算して、新たな論理関数Ｆ’を生成し、再度ステップＳ７で充足可能性判定器５に解かせる必要がある。
【００２５】
具体例を図８に示す。充足解Ａ８は既に１度出力されたので、もう一度同じ解を表示する必要はない。しかし、論理関数Ｆのままでは充足可能性判定器５は再び充足解Ａ８を出力する可能性がある。そこで、以下のように表示される充足解の候補から充足解Ａ８を除外する。
Ｆ’＝Ｆ∧〜Ａ８                                                    (5)
図８の表から、「Ａ８＝〜ａ∧〜ｂ∧〜ｃ∧〜ｍ∧〜ｎ∧〜ｏ∧ｐ∧ｑ∧ｒ∧ｓ∧ｅ」なので、「〜Ａ８＝〜（〜ａ∧〜ｂ∧〜ｃ∧〜ｍ∧〜ｎ∧〜ｏ∧ｐ∧ｑ∧ｒ∧ｓ∧ｅ）」となり、二重否定をなくすと、ド・モルガンの法則により、以下のように表される。
〜Ａ８＝ａ∨ｂ∨ｃ∨ｍ∨ｎ∨ｏ∨〜ｐ∨〜ｑ∨〜ｒ∨〜ｓ∨〜ｅ        (6)
式(6)を式(5)に代入してＦ’を解くと、充足解Ａ８以外の別解を得ることができる。図８は、充足解Ａ８の次に充足解Ａ３が得られた例を示している。
【００２６】
以下、同様に一度表示出力された充足解を除外し、ＵＮＳＡＴｉｓｆｉａｂｌｅが表示されるまで繰り返し充足可能性判定のステップＳ７を実施する。充足解が存在する限り新たなテスト制約を生成し、別解探索・記憶装置７に保存することができる。本実施例では、Ａ１〜Ａ８のすべてを出力後、ＵＮＳＡＴｉｓｆｉａｂｌｅと表示されるので、その時点で処理を終了する。
【００２７】
以上のように、本実施例は、ＳＡＴ手法を応用してゴールデンを解析することにより、機能検証を行う際に、検証目的に合致するテスト制約を複数組自動抽出することができる。また、必ずしも仕様を熟知していなくてもテスト制約を抽出することができる。抽出したテスト制約は、ソフトウェアのテストだけでなく、ハードウェアの機能検証にも用いることができる。さらに、抽出したテスト制約は、テスト・シーケンスの作成にも活用することができるる。
【符号の説明】
【００２８】
１：入力装置
２：制御構造生成装置
３：制御経路分析装置
４：論理関数構成装置
５：充足可能性判定器
６：出力装置
７：別解探索・記憶装置
８：制御装置
９：信号線
【先行技術文献】
【非特許文献】
【００２９】
【非特許文献１】Ben Chelf and Andy Chou, “The Next Generation of Static Analysis (Boolean Satisfiability and Path Simulation − A Perfect Match)”, White Paper, Coverity, Inc.、[平成２１年３月１７日検索]、インターネット＜URL： http://www.coverity.com/html_ja/research-library.html ＞(ブール充足可能性：次世代の静的解析)
【図１】
2010238057.tif 000003
【図２】
2010238057.tif 000004
【図３】
2010238057.tif 000005
【図４】
2010238057.tif 000006
【図５】
2010238057.tif 000007
【図６】
2010238057.tif 000008
【図７】
2010238057.tif 000009
【図８】
2010238057.tif 000010