(57)【特許請求の範囲】
【請求項１】
検査対象のソフトウェアと、前記ソフトウェアへの入力値の検査範囲とする入力値制約条件と、ソフトウェアが満たすべき要件を指定する検査条件と、を入力値として受け取り、該入力値に基づいてソフトウェアを検査し、検査条件判定結果を出力するソフトウェア検査装置であって、
制約条件付き最適化ソルバを用いた充足可能性判定により前記ソフトウェアの検査を実行し、
前記ソルバは、
前記入力値制約条件の範囲でのプログラム実行過程で演算時オーバーフローが発生する場合には、オーバーフローを招く演算箇所を出力する機能と、
前記検査条件に違反する不正な入力値がある場合には、前記検査条件違反を導くプログラム実行経路を出力する機能と、を有し、
前記ソフトウェアを制約条件付き半順序グラフ化SSA形式に変換し、さらに前記入力値制約条件と前記検査条件を併合して制約形式のリストを生成する機能と、
前記制約形式のリストから、値域制約付き制約条件式のリストおよび前記制約条件式の一階及び二階導関数式を生成する機能と、
前記制約条件付き数値最適化ソルバからの出力値を、演算時オーバーフローの発生有無の報告、および前記検査条件の判定結果の報告に変換する機能と、
を備える事を特徴とするソフトウェア検査装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアを検査する技術に関する。
【背景技術】
【０００２】
近年、モデル検査手法と呼ばれる入出力関係を動的に解析する手法が効果的であることが知られるようになってきた。モデル検査手法は、ソフトウェア００２に対する入力値とソフトウェア００２の内部状態により出力値が動的に決定されるソフトウェア００２モデルを構築し、モデルから時系列に出力される出力値列として観察されるソフトウェア００２の動的挙動の妥当性を評価する手法である。これにより、機能要件および安全性要件に違反する不具合に相当する入力値または内部状態が存在することを探索する。【０００３】
モデル検査手法は、ソフトウェア００２の内部状態を記述する内部状態値を定義し、ソフトウェア００２の入出力関係に対応する状態遷移規則を実装した状態遷移モデルを用いて、不具合に相当する状態遷移列を発見するという意味で、動的な入出力関係解析手法である。下記特許文献１は、モデル検査手法に係る従来技術を記載している。【０００４】
特に、解析の高速化の為に、充足可能性判定機能を用いたソフトウェア検査装置００１が開示されている。状態値をビット値化し、ビットレベルで二分木探索をする(Boolean SAT)ソルバと、背景論理を用いた充足可能性をするＳＭＴ（Satisfiability Modulo Theory）ソルバを用いる方法が知られている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２０１２−１５５５１７号公報  実際、ソースコードを対象としたモデル検査手法が、車載ソフトウェア００２の潜在的不具合を確実に検出する手段として有効である。車載ソフトウェア００２は、時系列に沿って与えられる入力値列に対して内部状態値列を演算し、出力値列を出力するものであるため、上述のモデル検査手法の特性とよく合致するからである。ＩＳＯ２６２６２規格においてもソフトウェア００２の認証要件を満たすことを証明する手段としてモデル検査手法を要請するようになっている。
【発明の概要】
【発明が解決しようとする課題】
【０００６】
モデル検査手法の有効性が知られているにも関わらず、解析に要する計算量の多さのため、大規模なソフトウェア００２を扱えないという課題がある。また、単純な四則演算よりも著しく複雑な演算をするプログラムを含む信号処理は制御ソフトウェア００２等でも同様の課題に直面している。状態値をビット値化する方式では、状態値の数が増えてしまい、拡張性を損なっている。また状態値は通常はビット値ではなく数バイト単位の定型データであり、二分木探索をしたとしても効率が悪い。この点を解決するために提案されたＳＭＴソルバを用いた方式であっても、背景論理として定義されていないプログラム処理部は扱えず、さらに実質的に、解析に要する計算量の削減効果が見込めない場合もある。
【課題を解決するための手段】
【０００７】
ソフトウェア００２のモデル検査問題を充足可能性判定問題に帰着させた上で、数値解析的に充足可能性を判定する方法が有効である。制約条件付き非線形計画法の問題を解く為に用いられるソルバは、所与の制約条件及び変数値に対する値域制約の元で、制約条件式を充足する解の有無を判定する機能を提供し、既存の方式よりも十分に高速に判定出来る。
【発明の効果】
【０００８】
既存の充足可能性判定問題を解くソルバを用いたモデル検査問題を、より短時間で解けるようになる。その為、大規模なプログラムに対してモデル検査手法を適用出来るようになる。
【図面の簡単な説明】
【０００９】
【図１】ソフトウェア検査装置００１
【図２】ソフトウェア検査装置００１の処理フロー
【図３】入力値制約条件００３、ソフトウェア００２、検査条件の例
【図４】制御フローグラフ表現
【図５】半順序グラフ化ＳＳＡ形式の構成要素
【図６】半順序グラフ化ＳＳＡ形式の例
【図７】ループ展開による再帰処理を含む制御フローグラフの半順序グラフ化
【図８】入力値制約・検査条件併合、制約形式のリスト生成
【図９】制約形式のリスト
【図１０】ソフトウェア００２検査に用いる充足可能性判定問題
【図１１】制約条件付き数値最適化ソルバのインターフェース
【図１２】プログラム内変数/ソルバ内変数変換テーブル 
【図１３】ソルバ内変数値域制約生成
【図１４】制約形式毎の導関数式生成
【図１５】演算時オーバーフロー検出用の検査条件
【図１６】数値最適化ソルバ用制約形式変換部からの出力情報
【図１７】論理和で連結した制約形式から論理積で連結した制約形式への変換
【発明を実施するための形態】
【００１０】
本発明を実現する具体的な手順を以下に開示する。
＜実施の形態＞
図１はソフトウェア検査装置００１内部の構成、入力、および出力情報を示す。
【００１１】
ソフトウェア検査装置００１は、検査対象のソフトウェア００２、前記ソフトウェア００２に対する入力値制約条件００３、および前記ソフトウェア００２に関する検査条件００４を入力として、検査条件判定結果００５を出力する。
【００１２】
ソフトウェア００２は、プログラム内部状態値の初期値、および外部から受けとる入力値列により、一意に出力値列を決定するものである。その為、入力値制約条件００３は、プログラム内部状態値の初期値、および入力値列の取りうる自由度を制限し、実際にソフトウェア００２が受け取るとした前提条件に相当する制約条件を指定する。この事により、異常な初期値や異常な入力値列を入力された前記ソフトウェア００２が、異常な出力値列を出力して、当然の帰結として前記検査条件に違反するといった、ソフトウェア検査装置００１の誤判定を解決する為に用いるものである。
【００１３】
ソフトウェア検査装置００１は、制約条件付きSSA(Static Single Assignment)形式変換部００１１、制約条件付き数値最適化ソルバ用制約形式変換部００１２、制約条件付き数値最適化ソルバ００１３、および検査条件判定結果出力部００１４で構成される。
図２は、ソフトウェア検査装置００１の処理フローを示す。
【００１４】
本実施例では、既存手法との構成上の差異が、主として充足可能性判定問題の解法にあることを明確にするために、Bounded Model Checkingとして知られている既存のモデル検査手法において通常用いられる手順であって、ソフトウェア００２の中間表現の一つであるSSA(Static Single Assignment)形式を経て充足可能性判定問題に還元する手順を継承する。SSA形式に変換する手順は、検査対象のソフトウェア００２の言語構造が主として手続き型言語である場合に適したモデル検査手法であり、一例として関数型言語で記述されたソフトウェア００２を検査する場合には、最終的に充足可能性判定問題に還元される限りは、言語構造に即した別の中間表現を用いてもよい。
【００１５】
制約条件付きSSA形式変換部００１１は、ソフトウェア００２をパースツリーに変換し、制御フローグラフを構築した上でSSA形式の中間表現に変換する。続いて、ソフトウェア００２に含まれる分岐条件、及びループに代表される再帰実行処理部を展開して、分岐条件式および演算を通じた割り当て式のみで構成される半順序グラフ化SSA形式に変換するステップ００１１０１、続いて、前記半順序グラフ化SSA形式に対して、指定した入力値制約条件００３と検査条件００４を併合して、制約形式のリストを生成するステップ００１１０２を経て、検査条件００４を含まない制約形式のリストF1と、検査条件００４を含む制約形式のリストF2の二つを出力する。
【００１６】
この手順は既知の手法ではあるものの、本発明の適用を容易にする為、変換過程の具体的な例を図３から図７にて示す。
【００１７】
図３は、制約条件付きSSA形式変換部００１１に入力する情報の例である。
構造化プログラム定理の為、一般的に手続き型言語のソフトウェア００２は、順序付けられた演算手続き、分岐条件、および再帰条件を組み合わせて表現する事が出来る。ソフトウェア００２に対する入力値ｘを限定する入力値制約条件００３、および検査対象ソフトウェア００２からの返り値ｚやプログラム内部状態値ｘ、ｙ、ｚ、ｗについて検査したい検査条件００４を指定する。検査条件００４は通常、ソフトウェア００２が満たすべき振る舞いを記述する機能要件や、ソフトウェア００２の安全要件等から導かれる動作制約等が用いられる。
【００１８】
図４は、ソフトウェア００２をパースし、制御フローグラフを構築したものである。本グラフを構成するノードは、図５に示される構成要素を含む。つまり、開始地点、SSA割り当て式、分岐評価式、ファイ関数と呼称される分岐終了式、および終了地点で構成される。再帰処理は分岐経路が局所的に循環グラフとなる特殊な構造の場合に相当する。
【００１９】
図６はSSA形式に変換して、開始地点から終了地点までの実行順序が位置方向となるように再構築した、半順序グラフ化SSA形式に変換した結果を示す。SSA形式の特徴は、演算を通じてプログラム内変数に演算結果を格納するたびに、新規の変数を設定していく事である。
【００２０】
図７は、whileループ文に代表される再帰実行処理をする方法であって、loop unwindingと呼称される手法を適用して再構築した、半順序グラフ化SSA形式である。既知のBounded Model検査手法では、ループのある箇所毎に再帰実行する回数の上限値を設定し、再帰実行回数毎に分岐条件を逐次追加することで、図６と同様の半順序グラフ化SSA形式に還元する。
【００２１】
図８は、ステップ００１１０２の詳細な手順を示す。
【００２２】
ステップ00110201 にて、半順序グラフ化SSA形式の、ソフトウェア００２の中間表現を取得する。
【００２３】
ここで、SSA割り当て式に代表される、演算を通じて限定されるプログラム内変数間の関係を制約形式と呼称する。指定した入力値制約条件００３も同様に、プログラム内変数に対する制約形式とみなすことが出来る。
【００２４】
新規に定義した空のリストFに、この入力値制約条件００３に相当する制約形式を追加する。
【００２５】
引き続き、前記半順序化SSA形式のプログラム中間表現の開始地点から順に構成要素を読み込む。
【００２６】
評価式ECがSSA割り当て式である場合（ステップ00110202）には、割り当て式を前記リストFに追加し、評価式EDがSSA分岐評価式である場合（ステップ00110203）では、分記先の数だけ（一例として２つを例に説明する）、新規に空の制約形式のリストFp、Fqを生成して、分岐評価式が真である事を表現する制約形式、及び偽であることを表現する制約形式をそれぞれ登録する。分岐処理が終了する地点まで、それぞれの制約形式のリストFp,Fqに、SSA割り当て式に対応する制約形式を追加していく。
【００２７】
分岐処理の完了時点で、前記制約形式のリストFに、F1とF2の論理和をとった制約形式(Fp||Fq)を追加し、ファイ関数と呼称されるSSA分岐終了式を追加する。終了地点出ない限りは本手続きを継続して、制約形式のリストFを更新する。
【００２８】
終了時点に到達したら、ステップ００１１０２０３にて、制約形式のリストFをコピーしてF1とし、検査条件００４を含まない制約形式のリストとして出力する。続いてステップ００１１０２０４では、検査条件００４を制約形式に変換し、これの否定論理をとった前記制約形式を、リストFに追加して、制約形式F2として出力して終了する。
【００２９】
図６にて例示した半順序グラフ化SSA形式から生成された制約形式のリストであって、検査条件を含むものは、図９に開示される通りである。
【００３０】
なお、既存のモデル検査手法は、図１０に示される式の充足解を探索する問題に還元させるものである。SSA形式に変換した時点で逐次割り当てされたプログラム内変数をビット値化して、充足解を探索するBooleanSATソルバを用いる方法、および背景論理を用いて制約形式のリストを縮約して、ビット値化して充足解を探索する場合よりは小規模な充足可能性判定問題を解くＳＭＴソルバを用いる手法が、個の充足可能性判定問題を解く手段として用いられている。
【００３１】
図２に戻り、ソフトウェア検査装置００１の処理フローの説明を続ける。
【００３２】
数値最適化ソルバ用制約形式変換部００１２は、この二つの制約形式のリストF１とF2を受け取り、充足可能性判定をする数値最適化ソルバが処理できる形式に変換する。
【００３３】
本発明は、図９に例示した制約条件のリストを一種の連立方程式と捉え直し、連立方程式の解を数値的に算出することで、ＢｏｏｌｅａｎＳＡＴソルバおよびＳＭＴソルバよりも十分に高速に、充足可能性を判定する、つまり連立方程式を解ける点を活用したものである。
【００３４】
図１１は、制約条件付き数値最適化ソルバ００１３のインターフェースを示す。
【００３５】
入力情報は、目的関数ｆ、未定変数Ｘ、および制約条件式ｇで構成される。
【００３６】
制約条件付き数値最適化ソルバ００１３は、すべての制約条件式を充足する割り当て値Ｘがある場合には、具体的な割り当て値を報告し、充足解が無い場合には、前記制約条件式ｇの内、充足不能にであった制約条件式のリストと、最終的な割り当て値Ｘを報告する。
【００３７】
前記の未定変数Ｘは、浮動小数点数等で実装される連続値と、整数値を含む。整数値を含む制約条件付き数値最適化ソルバは、特別にＭＩＮＬＰ（ＭｉｘｅｄＩｎｔｅｇｅｒＮｏｎｌｉｎｅａｒ  Ｐｒｏｇｒａｍｍｉｎｇ）ソルバと呼称されている。
【００３８】
目的関数ｆの引数となる未定変数それぞれに関する一階導関数を用いることで、高速かつ正確な評価が出来るようになる。自動微分手法及び局所数値微分等の手法で、厳密な一階導関数の指定を必要としないソルバもあるが、評価時間の短縮のためには、一階導関数を指定する事が望ましい。同様に、充足解が無い場合には無い事を保証する為に、未定変数には上下限の値域制約を付加して、評価範囲を有界にする。
【００３９】
同様に、制約条件式にも上下限値、１階および２階導関数を指定する事で、高速かつ正確な評価をする事が出来る。
【００４０】
前記制約条件式が微分可能でなく、検査範囲とした値域内で一階導関数が定義出来ない場合には、不連続になる点で分割し、分岐条件を含む制約形式に置換すればよい。
【００４１】
本実施例における制約条件付き数値最適化ソルバ０１３は、一般的には、複数の制約形式の論理和、及び論理積で連結した制約形式のリストに対して充足可能性を判定出来る。しかし、本質的に組み合わせ複雑性を持ち、これを効率的に処理する方法は確立していない。既存のソルバは、内部で分岐条件毎に部分問題に分割し、論理積だけで連結した問題を生成している。これは、設定した制約条件式の論理積に関する充足可能性であれば、最悪でも変数の数に対して多項式時間で判定出来るためである。
【００４２】
実際、図９に例示される通り、分岐条件を含むソフトウェア００２から生成した制約形式は、論理和で連結した制約形式を一部に含む。そこで、本実施例では、分岐条件毎に問題を分割して、論理積で連結された複数の問題を生成する方法と、論理和で連結された制約形式群を、補助変数を導入して、論理積で連結した制約形式群に書き換える二つの方法を示しておく。
【００４３】
このソルバ００１３のインターフェースに合致するように、制約形式のリストＦ１，およびＦ２を変換する。
【００４４】
ステップ００１２０１では、制約形式のリストの各要素に導入された、SSA形式のプログラム内変数と数値最適化ソルバ内変数の対応関係を保持する変換テーブルを構築する。図９に例示した制約形式のリストから構築した例が、図１２に示されている。
【００４５】
プログラム内変数は通常、型と値域を持つ。四則演算に代表される、値域を逸脱するような演算に対しては、ソフトウェア００２は予期しない振る舞いをするため、検査条件００４を評価する前に、値域を逸脱しない事を確認するためにこの型情報を用いる。
【００４６】
ステップ００１２０２では、この型情報から制約条件付き数値最適化ソルバ００１３のインターフェース内未定変数の値域を導きだし、図１３に例示されるような変数値域制約を設定して制約条件付き数値最適化ソルバ００１３に渡す。
【００４７】
同様に、ステップ００１２０３では、制約形式のリストの各構成要素から、ステップ001201で構築したプログラム内変数/ソルバ内変数変換テーブルを用いて、制約条件式の生成、および導関数群を生成する。
【００４８】
検査条件を含まない制約形式のリストＦ１と検査条件を含む制約形式のリストＦ２それぞれを変換して、数値最適化ソルバ用制約形式Ｐ１，およびＰ２を得る。
【００４９】
ステップ００１２０４では制約形式のリストＰ１に対してさらに、未定変数Ｘの値域制約条件を外し、図１５に示した演算時オーバーフロー検出用の検査条件をする。
【００５０】
図１６は、数値最適化ソルバ用制約形式Ｐ１，およびＰ２の一例であって、プログラム内に分岐条件を含む場合の典型的な構成を示す。前記数値最適化ソルバ用制約形式P1,P2は、分岐条件毎に充足可能性判定問題を分割して論理和で連結したものとして構成される。
【００５１】
この個々の数値最適化ソルバ用制約形式P1-1〜P1-X,P2-1〜P2-Yを並列実行が他計算機で評価して、いずれか一つ以上の制約形式の充足解があるか否かを判定する。
【００５２】
また、前述の演算時オーバーフロー検出用の検査条件に例示されるように、複数の制約形式を論理積で結合した検査条件を用いる場合、否定論理をとった制約形式が充足可能性判定問題に組み込まれる為、制約形式の論理和を含む。数値最適化ソルバは論理積だけで連結された場合には高速に処理出来るため、制約形式の論理積だけで構成される式に変換する必要がある。この際、図１７に示されるように、いくつかの補助変数をソルバ内変数のリストに追加して、論理和で連結した制約形式を、論理積で連結した制約形式に変換すればよい。複数の制約形式の論理和をとった制約形式を論理積で結合した形式は、CNF形式(Conjunctive Normal Form)と呼称されている。複数の制約形式の論理積をとった制約形式を論理和で結合した形式はDNF形式（Disjunctive Normal Form）と呼称されている。多数の制約形式を任意に論理和・論理積・否定論理で連結したものは、機械的にCNF形式およびDNF形式に変換できる事が知られている。
【００５３】
数値最適化ソルバ用制約形式Ｐ１，およびＰ２をソルバ００１３に渡し、充足可能性を評価する。検査条件判定結果出力部００１４は、充足解の有無とその解釈をして、検査条件判定結果００５を出力する。
【００５４】
判定内容は、演算時オーバーフローに代表される、プログラム内変数の型毎に定義された値域を逸脱する場合の有無を判定する事、および指定の入力値制約条件００３の下で、検査条件００４に違反するようなプログラム実行経路の有無を判定する事である。
【００５５】
ステップ００１４０１では、事前にプログラム内変数の型毎に定義された値域を逸脱する場合の有無を判定する。このステップは、実際のプログラム変数に対する演算時オーバーフローの結果得られる返り値と、上下限境界値がないソルバ内変数との間で乖離する事に起因した誤判定を防ぐために必要である。
【００５６】
充足解がある場合は、入力値制約条件００３の元で任意に取りうる値に対し、ステップ００１２０２で指定したソルバ内変数値域を超える演算が起こる事を意味する。
【００５７】
ソフトウェア００２が手続き型言語である為に、入力値制約条件００３の元で指定された値を受け取って演算を進める過程で、演算結果を受け取る返り値は必ず存在するにも関わらず充足解が無い事を意味する。その原因は、ステップ００１２０２で追加した制約条件が充足できない事であり、返り値に対応するプログラム内変数が、指定の型情報により限定される値域の上下限値の範囲内に収まらないためである。
【００５８】
この場合、ステップ００１４０２に進み、充足不能判定時点でのソルバ内変数の割り当て値のリストを取得し、ステップ００１２０１出構築したプログラム内変数/ソルバ内変数変換テーブルを用いて、プログラム内変数の割り当て値のリストに逆変換する。
【００５９】
この逆変換の過程で、ステップ００１２０２で指定した値域を逸脱するプログラム変数の位置を特定する。最後に、ステップ００５１に進み、演算時オーバーフローの報告およびオーバーフローした前記プログラム内変数を出力して終了する。
【００６０】
一方、ステップ００１４０１で評価結果を取得し、充足解が無い場合には、演算時オーバーフローがなく、検査対象のソルバ内変数空間内の検査範囲が連結しており、プログラム変数の型の値域に依存した意図しない演算結果を招かない事が確認された。この場合には、ステップ００１４０３に進む。
【００６１】
ステップ００１４０３では数値最適化ソルバ用制約形式P2の充足解の有無の評価結果を取得する。充足解が無い場合は、指定の検査条件を満たすことを報告して終了する。
【００６２】
一方、充足解がある場合には、背理法により、入力値制約条件００３で限定したソフトウェア００２への入力値であって、検査条件００４に違反する不正な入力値が存在する事を意味する。この場合にはステップ００１４０４に進み、同様に、制約形式を満たすソルバ内変数の割り当て値のリストから、プログラム内変数の割り当て値のリストに逆変換する。これを用いて、検査条件００４の違反に到るプログラム実行経路を生成し、検査条件判定結果００５として報告して終了する。
【符号の説明】
【００６３】
００１  ソフトウェア検査装置００１
００２  ソフトウェア００２
００３  入力値制約条件００３
００４  検査条件
００５  検査条件判定結果
００１１  制約条件付きSSA形式変換部
００１２  制約条件付き数値最適化ソルバ用制約形式変換部
００１３  制約条件付き数値最適化ソルバ
００１４  検査条件判定結果出力部
【図１】
0006469730.tif 000002
【図２】
0006469730.tif 000003
【図３】
0006469730.tif 000004
【図４】
0006469730.tif 000005
【図５】
0006469730.tif 000006
【図６】
0006469730.tif 000007
【図７】
0006469730.tif 000008
【図８】
0006469730.tif 000009
【図９】
0006469730.tif 000010
【図１０】
0006469730.tif 000011
【図１１】
0006469730.tif 000012
【図１２】
0006469730.tif 000013
【図１３】
0006469730.tif 000014
【図１４】
0006469730.tif 000015
【図１５】
0006469730.tif 000016
【図１６】
0006469730.tif 000017
【図１７】
0006469730.tif 000018