図面 (/)

技術 ソフトウェア検査装置

出願人 株式会社日立製作所
発明者 西昌能
出願日 2015年1月30日 (4年7ヶ月経過) 出願番号 2016-571615
公開日 2017年10月5日 (1年11ヶ月経過) 公開番号 WO2016-121074
状態 特許登録済
技術分野 デバッグ/監視
主要キーワード 背理法 演算手続き 動作制約 階導関数 数値微分 本手続き 変数空間 状態遷移規則
関連する未来課題
重要な関連分野

この項目の情報は公開日時点(2017年10月5日)のものです。
また、この項目は機械的に抽出しているため、正しく解析できていない場合があります

図面 (18)

課題・解決手段

ソフトウェアの不具合を検出するための手段としてモデル検査手法の有効性が知られているにも関わらず、検査に要する計算量の多さのため、大規模なソフトウェアを扱えない。 ソフトウェアのモデル検査問題を充足可能性判定問題に帰着させた上で、制約条件付き通知最適化問題解く為に用いられるソルバが前記問題を解ける形に変換して、数値解析的に充足可能性を判定する。

概要

背景

近年、モデル検査手法と呼ばれる入出力関係を動的に解析する手法が効果的であることが知られるようになってきた。モデル検査手法は、ソフトウェア002に対する入力値とソフトウェア002の内部状態により出力値が動的に決定されるソフトウェア002モデル構築し、モデルから時系列に出力される出力値列として観察されるソフトウェア002の動的挙動妥当性を評価する手法である。これにより、機能要件および安全性要件違反する不具合に相当する入力値または内部状態が存在することを探索する。

モデル検査手法は、ソフトウェア002の内部状態を記述する内部状態値を定義し、ソフトウェア002の入出力関係に対応する状態遷移規則実装した状態遷移モデルを用いて、不具合に相当する状態遷移列発見するという意味で、動的な入出力関係解析手法である。下記特許文献1は、モデル検査手法に係る従来技術を記載している。

特に、解析の高速化の為に、充足可能性判定機能を用いたソフトウェア検査装置001が開示されている。状態値ビット値化し、ビットレベル二分木探索をする(Boolean SAT)ソルバと、背景論理を用いた充足可能性をするSMT(Satisfiability Modulo Theory)ソルバを用いる方法が知られている。

概要

ソフトウェアの不具合を検出するための手段としてモデル検査手法の有効性が知られているにも関わらず、検査に要する計算量の多さのため、大規模なソフトウェアを扱えない。 ソフトウェアのモデル検査問題を充足可能性判定問題に帰着させた上で、制約条件付き通知最適化問題解く為に用いられるソルバが前記問題を解ける形に変換して、数値解析的に充足可能性を判定する。

目的

効果

実績

技術文献被引用数
0件
牽制数
0件

この技術が所属する分野

ライセンス契約や譲渡などの可能性がある特許掲載中! 開放特許随時追加・更新中 詳しくはこちら

請求項1

検査対象ソフトウェアと、前記ソフトウェアへの入力値検査範囲とする入力値制約条件と、ソフトウェアが満たすべき要件を指定する検査条件と、を入力値として受け取り、該入力値に基づいてソフトウェアを検査し、検査条件判定結果を出力するソフトウェア検査装置であって、制約条件付き最適化ソルバを用いた充足可能性判定により前記ソフトウェアの検査を実行するソフトウェア検査装置。

請求項2

前記ソルバは、前記入力値制約条件の範囲でのプログラム実行過程演算オーバーフローが発生する場合には、オーバーフローを招く演算箇所を出力する機能と、前記検査条件に違反する不正な入力値がある場合には、前記検査条件違反を導くプログラム実行経路を出力する機能と、を有する請求項1に記載のソフトウェア検査装置。

請求項3

前記ソフトウェアを制約条件付き半順序グラフ化SSA形式に変換し、さらに前記入力値制約条件と前記検査条件を併合して制約形式リストを生成する機能と、前記制約形式のリストから、値域制約付制約条件式のリストおよび前記制約条件式の一階及び二階導関数式を生成する機能と、前記制約条件付き数値最適化ソルバからの出力値を、演算時オーバーフローの発生有無報告、および前記検査条件の判定結果の報告に変換する機能と、備える事を特徴とする請求項2に記載のソフトウェア検査装置。

技術分野

0001

本発明は、ソフトウェア検査する技術に関する。

背景技術

0002

近年、モデル検査手法と呼ばれる入出力関係を動的に解析する手法が効果的であることが知られるようになってきた。モデル検査手法は、ソフトウェア002に対する入力値とソフトウェア002の内部状態により出力値が動的に決定されるソフトウェア002モデル構築し、モデルから時系列に出力される出力値列として観察されるソフトウェア002の動的挙動妥当性を評価する手法である。これにより、機能要件および安全性要件違反する不具合に相当する入力値または内部状態が存在することを探索する。

0003

モデル検査手法は、ソフトウェア002の内部状態を記述する内部状態値を定義し、ソフトウェア002の入出力関係に対応する状態遷移規則実装した状態遷移モデルを用いて、不具合に相当する状態遷移列発見するという意味で、動的な入出力関係解析手法である。下記特許文献1は、モデル検査手法に係る従来技術を記載している。

0004

特に、解析の高速化の為に、充足可能性判定機能を用いたソフトウェア検査装置001が開示されている。状態値ビット値化し、ビットレベル二分木探索をする(Boolean SAT)ソルバと、背景論理を用いた充足可能性をするSMT(Satisfiability Modulo Theory)ソルバを用いる方法が知られている。

先行技術

0005

特開2012−155517号公報 実際、ソースコードを対象としたモデル検査手法が、車載ソフトウェア002の潜在的不具合を確実に検出する手段として有効である。車載ソフトウェア002は、時系列に沿って与えられる入力値列に対して内部状態値列演算し、出力値列を出力するものであるため、上述のモデル検査手法の特性とよく合致するからである。ISO26262規格においてもソフトウェア002の認証要件を満たすことを証明する手段としてモデル検査手法を要請するようになっている。

発明が解決しようとする課題

0006

モデル検査手法の有効性が知られているにも関わらず、解析に要する計算量の多さのため、大規模なソフトウェア002を扱えないという課題がある。また、単純な四則演算よりも著しく複雑な演算をするプログラムを含む信号処理制御ソフトウェア002等でも同様の課題に直面している。状態値をビット値化する方式では、状態値の数が増えてしまい、拡張性を損なっている。また状態値は通常はビット値ではなく数バイト単位定型データであり、二分木探索をしたとしても効率が悪い。この点を解決するために提案されたSMTソルバを用いた方式であっても、背景論理として定義されていないプログラム処理部は扱えず、さらに実質的に、解析に要する計算量の削減効果が見込めない場合もある。

課題を解決するための手段

0007

ソフトウェア002のモデル検査問題を充足可能性判定問題に帰着させた上で、数値解析的に充足可能性を判定する方法が有効である。制約条件付き非線形計画法の問題を解く為に用いられるソルバは、所与の制約条件及び変数値に対する値域制約の元で、制約条件式充足する解の有無を判定する機能を提供し、既存の方式よりも十分に高速に判定出来る。

発明の効果

0008

既存の充足可能性判定問題を解くソルバを用いたモデル検査問題を、より短時間で解けるようになる。その為、大規模なプログラムに対してモデル検査手法を適用出来るようになる。

図面の簡単な説明

0009

ソフトウェア検査装置001
ソフトウェア検査装置001の処理フロー
入力値制約条件003、ソフトウェア002、検査条件の例
制御フローグラフ表現
半順序グラフ化SSA形式の構成要素
半順序グラフ化SSA形式の例
ループ展開による再帰処理を含む制御フローグラフの半順序グラフ化
入力値制約・検査条件併合、制約形式リスト生成
制約形式のリスト
ソフトウェア002検査に用いる充足可能性判定問題
制約条件付き数値最適化ソルバのインターフェース
プログラム内変数/ソルバ内変数変換テーブル
ソルバ内変数値域制約生成
制約形式毎の導関数式生成
演算時オーバーフロー検出用の検査条件
数値最適化ソルバ用制約形式変換部からの出力情報
論理和で連結した制約形式から論理積で連結した制約形式への変換

実施例

0010

本発明を実現する具体的な手順を以下に開示する。
<実施の形態>
図1はソフトウェア検査装置001内部の構成、入力、および出力情報を示す。

0011

ソフトウェア検査装置001は、検査対象のソフトウェア002、前記ソフトウェア002に対する入力値制約条件003、および前記ソフトウェア002に関する検査条件004を入力として、検査条件判定結果005を出力する。

0012

ソフトウェア002は、プログラム内部状態値の初期値、および外部から受けとる入力値列により、一意に出力値列を決定するものである。その為、入力値制約条件003は、プログラム内部状態値の初期値、および入力値列の取りうる自由度を制限し、実際にソフトウェア002が受け取るとした前提条件に相当する制約条件を指定する。この事により、異常な初期値や異常な入力値列を入力された前記ソフトウェア002が、異常な出力値列を出力して、当然の帰結として前記検査条件に違反するといった、ソフトウェア検査装置001の誤判定を解決する為に用いるものである。

0013

ソフトウェア検査装置001は、制約条件付きSSA(Static Single Assignment)形式変換部0011、制約条件付き数値最適化ソルバ用制約形式変換部0012、制約条件付き数値最適化ソルバ0013、および検査条件判定結果出力部0014で構成される。
図2は、ソフトウェア検査装置001の処理フローを示す。

0014

本実施例では、既存手法との構成上の差異が、主として充足可能性判定問題の解法にあることを明確にするために、Bounded Model Checkingとして知られている既存のモデル検査手法において通常用いられる手順であって、ソフトウェア002の中間表現の一つであるSSA(Static Single Assignment)形式を経て充足可能性判定問題に還元する手順を継承する。SSA形式に変換する手順は、検査対象のソフトウェア002の言語構造が主として手続き型言語である場合に適したモデル検査手法であり、一例として関数型言語で記述されたソフトウェア002を検査する場合には、最終的に充足可能性判定問題に還元される限りは、言語構造に即した別の中間表現を用いてもよい。

0015

制約条件付きSSA形式変換部0011は、ソフトウェア002をパースツリーに変換し、制御フローグラフを構築した上でSSA形式の中間表現に変換する。続いて、ソフトウェア002に含まれる分岐条件、及びループに代表される再帰実行処理部を展開して、分岐条件式および演算を通じた割り当て式のみで構成される半順序グラフ化SSA形式に変換するステップ001101、続いて、前記半順序グラフ化SSA形式に対して、指定した入力値制約条件003と検査条件004を併合して、制約形式のリストを生成するステップ001102を経て、検査条件004を含まない制約形式のリストF1と、検査条件004を含む制約形式のリストF2の二つを出力する。

0016

この手順は既知の手法ではあるものの、本発明の適用を容易にする為、変換過程の具体的な例を図3から図7にて示す。

0017

図3は、制約条件付きSSA形式変換部0011に入力する情報の例である。
構造化プログラム定理の為、一般的に手続き型言語のソフトウェア002は、順序付けられた演算手続き、分岐条件、および再帰条件を組み合わせて表現する事が出来る。ソフトウェア002に対する入力値xを限定する入力値制約条件003、および検査対象ソフトウェア002からの返り値zやプログラム内部状態値x、y、z、wについて検査したい検査条件004を指定する。検査条件004は通常、ソフトウェア002が満たすべき振る舞いを記述する機能要件や、ソフトウェア002の安全要件等から導かれる動作制約等が用いられる。

0018

図4は、ソフトウェア002をパースし、制御フローグラフを構築したものである。本グラフを構成するノードは、図5に示される構成要素を含む。つまり、開始地点、SSA割り当て式、分岐評価式、ファイ関数呼称される分岐終了式、および終了地点で構成される。再帰処理は分岐経路局所的に循環グラフとなる特殊な構造の場合に相当する。

0019

図6はSSA形式に変換して、開始地点から終了地点までの実行順序が位置方向となるように再構築した、半順序グラフ化SSA形式に変換した結果を示す。SSA形式の特徴は、演算を通じてプログラム内変数に演算結果を格納するたびに、新規の変数を設定していく事である。

0020

図7は、whileループ文に代表される再帰実行処理をする方法であって、loop unwindingと呼称される手法を適用して再構築した、半順序グラフ化SSA形式である。既知のBounded Model検査手法では、ループのある箇所毎に再帰実行する回数の上限値を設定し、再帰実行回数毎に分岐条件を逐次追加することで、図6と同様の半順序グラフ化SSA形式に還元する。

0021

図8は、ステップ001102の詳細な手順を示す。

0022

ステップ00110201 にて、半順序グラフ化SSA形式の、ソフトウェア002の中間表現を取得する。

0023

ここで、SSA割り当て式に代表される、演算を通じて限定されるプログラム内変数間の関係を制約形式と呼称する。指定した入力値制約条件003も同様に、プログラム内変数に対する制約形式とみなすことが出来る。

0024

新規に定義した空のリストFに、この入力値制約条件003に相当する制約形式を追加する。

0025

引き続き、前記半順序化SSA形式のプログラム中間表現の開始地点から順に構成要素を読み込む。

0026

評価式ECがSSA割り当て式である場合(ステップ00110202)には、割り当て式を前記リストFに追加し、評価式EDがSSA分岐評価式である場合(ステップ00110203)では、分記先の数だけ(一例として2つを例に説明する)、新規に空の制約形式のリストFp、Fqを生成して、分岐評価式が真である事を表現する制約形式、及びであることを表現する制約形式をそれぞれ登録する。分岐処理が終了する地点まで、それぞれの制約形式のリストFp,Fqに、SSA割り当て式に対応する制約形式を追加していく。

0027

分岐処理の完了時点で、前記制約形式のリストFに、F1とF2の論理和をとった制約形式(Fp||Fq)を追加し、ファイ関数と呼称されるSSA分岐終了式を追加する。終了地点出ない限りは本手続きを継続して、制約形式のリストFを更新する。

0028

終了時点に到達したら、ステップ00110203にて、制約形式のリストFをコピーしてF1とし、検査条件004を含まない制約形式のリストとして出力する。続いてステップ00110204では、検査条件004を制約形式に変換し、これの否定論理をとった前記制約形式を、リストFに追加して、制約形式F2として出力して終了する。

0029

図6にて例示した半順序グラフ化SSA形式から生成された制約形式のリストであって、検査条件を含むものは、図9に開示される通りである。

0030

なお、既存のモデル検査手法は、図10に示される式の充足解を探索する問題に還元させるものである。SSA形式に変換した時点で逐次割り当てされたプログラム内変数をビット値化して、充足解を探索するBooleanSATソルバを用いる方法、および背景論理を用いて制約形式のリストを縮約して、ビット値化して充足解を探索する場合よりは小規模な充足可能性判定問題を解くSMTソルバを用いる手法が、個の充足可能性判定問題を解く手段として用いられている。

0031

図2戻り、ソフトウェア検査装置001の処理フローの説明を続ける。

0032

数値最適化ソルバ用制約形式変換部0012は、この二つの制約形式のリストF1とF2を受け取り、充足可能性判定をする数値最適化ソルバが処理できる形式に変換する。

0033

本発明は、図9に例示した制約条件のリストを一種連立方程式と捉え直し、連立方程式の解を数値的に算出することで、BooleanSATソルバおよびSMTソルバよりも十分に高速に、充足可能性を判定する、つまり連立方程式を解ける点を活用したものである。

0034

図11は、制約条件付き数値最適化ソルバ0013のインターフェースを示す。

0035

入力情報は、目的関数f、未定変数X、および制約条件式gで構成される。

0036

制約条件付き数値最適化ソルバ0013は、すべての制約条件式を充足する割り当て値Xがある場合には、具体的な割り当て値を報告し、充足解が無い場合には、前記制約条件式gの内、充足不能にであった制約条件式のリストと、最終的な割り当て値Xを報告する。

0037

前記の未定変数Xは、浮動小数点数等で実装される連続値と、整数値を含む。整数値を含む制約条件付き数値最適化ソルバは、特別にMINLP(MixedIntegerNonlinear Programming)ソルバと呼称されている。

0038

目的関数fの引数となる未定変数それぞれに関する一階導関数を用いることで、高速かつ正確な評価が出来るようになる。自動微分手法及び局所数値微分等の手法で、厳密な一階導関数の指定を必要としないソルバもあるが、評価時間の短縮のためには、一階導関数を指定する事が望ましい。同様に、充足解が無い場合には無い事を保証する為に、未定変数には上下限の値域制約を付加して、評価範囲を有界にする。

0039

同様に、制約条件式にも上下限値、1階および2階導関数を指定する事で、高速かつ正確な評価をする事が出来る。

0040

前記制約条件式が微分可能でなく、検査範囲とした値域内で一階導関数が定義出来ない場合には、不連続になる点で分割し、分岐条件を含む制約形式に置換すればよい。

0041

本実施例における制約条件付き数値最適化ソルバ013は、一般的には、複数の制約形式の論理和、及び論理積で連結した制約形式のリストに対して充足可能性を判定出来る。しかし、本質的に組み合わせ複雑性を持ち、これを効率的に処理する方法は確立していない。既存のソルバは、内部で分岐条件毎に部分問題に分割し、論理積だけで連結した問題を生成している。これは、設定した制約条件式の論理積に関する充足可能性であれば、最悪でも変数の数に対して多項式時間で判定出来るためである。

0042

実際、図9に例示される通り、分岐条件を含むソフトウェア002から生成した制約形式は、論理和で連結した制約形式を一部に含む。そこで、本実施例では、分岐条件毎に問題を分割して、論理積で連結された複数の問題を生成する方法と、論理和で連結された制約形式群を、補助変数を導入して、論理積で連結した制約形式群に書き換える二つの方法を示しておく。

0043

このソルバ0013のインターフェースに合致するように、制約形式のリストF1,およびF2を変換する。

0044

ステップ001201では、制約形式のリストの各要素に導入された、SSA形式のプログラム内変数と数値最適化ソルバ内変数の対応関係を保持する変換テーブルを構築する。図9に例示した制約形式のリストから構築した例が、図12に示されている。

0045

プログラム内変数は通常、型と値域を持つ。四則演算に代表される、値域を逸脱するような演算に対しては、ソフトウェア002は予期しない振る舞いをするため、検査条件004を評価する前に、値域を逸脱しない事を確認するためにこの型情報を用いる。

0046

ステップ001202では、この型情報から制約条件付き数値最適化ソルバ0013のインターフェース内未定変数の値域を導きだし、図13に例示されるような変数値域制約を設定して制約条件付き数値最適化ソルバ0013に渡す。

0047

同様に、ステップ001203では、制約形式のリストの各構成要素から、ステップ001201で構築したプログラム内変数/ソルバ内変数変換テーブルを用いて、制約条件式の生成、および導関数群を生成する。

0048

検査条件を含まない制約形式のリストF1と検査条件を含む制約形式のリストF2それぞれを変換して、数値最適化ソルバ用制約形式P1,およびP2を得る。

0049

ステップ001204では制約形式のリストP1に対してさらに、未定変数Xの値域制約条件を外し、図15に示した演算時オーバーフロー検出用の検査条件をする。

0050

図16は、数値最適化ソルバ用制約形式P1,およびP2の一例であって、プログラム内に分岐条件を含む場合の典型的な構成を示す。前記数値最適化ソルバ用制約形式P1,P2は、分岐条件毎に充足可能性判定問題を分割して論理和で連結したものとして構成される。

0051

この個々の数値最適化ソルバ用制約形式P1-1〜P1-X,P2-1〜P2-Yを並列実行他計算機で評価して、いずれか一つ以上の制約形式の充足解があるか否かを判定する。

0052

また、前述の演算時オーバーフロー検出用の検査条件に例示されるように、複数の制約形式を論理積で結合した検査条件を用いる場合、否定論理をとった制約形式が充足可能性判定問題に組み込まれる為、制約形式の論理和を含む。数値最適化ソルバは論理積だけで連結された場合には高速に処理出来るため、制約形式の論理積だけで構成される式に変換する必要がある。この際、図17に示されるように、いくつかの補助変数をソルバ内変数のリストに追加して、論理和で連結した制約形式を、論理積で連結した制約形式に変換すればよい。複数の制約形式の論理和をとった制約形式を論理積で結合した形式は、CNF形式(Conjunctive Normal Form)と呼称されている。複数の制約形式の論理積をとった制約形式を論理和で結合した形式はDNF形式(Disjunctive Normal Form)と呼称されている。多数の制約形式を任意に論理和・論理積・否定論理で連結したものは、機械的にCNF形式およびDNF形式に変換できる事が知られている。

0053

数値最適化ソルバ用制約形式P1,およびP2をソルバ0013に渡し、充足可能性を評価する。検査条件判定結果出力部0014は、充足解の有無とその解釈をして、検査条件判定結果005を出力する。

0054

判定内容は、演算時オーバーフローに代表される、プログラム内変数の型毎に定義された値域を逸脱する場合の有無を判定する事、および指定の入力値制約条件003の下で、検査条件004に違反するようなプログラム実行経路の有無を判定する事である。

0055

ステップ001401では、事前にプログラム内変数の型毎に定義された値域を逸脱する場合の有無を判定する。このステップは、実際のプログラム変数に対する演算時オーバーフローの結果得られる返り値と、上下限境界値がないソルバ内変数との間で乖離する事に起因した誤判定を防ぐために必要である。

0056

充足解がある場合は、入力値制約条件003の元で任意に取りうる値に対し、ステップ001202で指定したソルバ内変数値域を超える演算が起こる事を意味する。

0057

ソフトウェア002が手続き型言語である為に、入力値制約条件003の元で指定された値を受け取って演算を進める過程で、演算結果を受け取る返り値は必ず存在するにも関わらず充足解が無い事を意味する。その原因は、ステップ001202で追加した制約条件が充足できない事であり、返り値に対応するプログラム内変数が、指定の型情報により限定される値域の上下限値の範囲内に収まらないためである。

0058

この場合、ステップ001402に進み、充足不能判定時点でのソルバ内変数の割り当て値のリストを取得し、ステップ001201出構築したプログラム内変数/ソルバ内変数変換テーブルを用いて、プログラム内変数の割り当て値のリストに逆変換する。

0059

この逆変換の過程で、ステップ001202で指定した値域を逸脱するプログラム変数の位置を特定する。最後に、ステップ0051に進み、演算時オーバーフローの報告およびオーバーフローした前記プログラム内変数を出力して終了する。

0060

一方、ステップ001401で評価結果を取得し、充足解が無い場合には、演算時オーバーフローがなく、検査対象のソルバ内変数空間内の検査範囲が連結しており、プログラム変数の型の値域に依存した意図しない演算結果を招かない事が確認された。この場合には、ステップ001403に進む。

0061

ステップ001403では数値最適化ソルバ用制約形式P2の充足解の有無の評価結果を取得する。充足解が無い場合は、指定の検査条件を満たすことを報告して終了する。

0062

一方、充足解がある場合には、背理法により、入力値制約条件003で限定したソフトウェア002への入力値であって、検査条件004に違反する不正な入力値が存在する事を意味する。この場合にはステップ001404に進み、同様に、制約形式を満たすソルバ内変数の割り当て値のリストから、プログラム内変数の割り当て値のリストに逆変換する。これを用いて、検査条件004の違反に到るプログラム実行経路を生成し、検査条件判定結果005として報告して終了する。

0063

001ソフトウェア検査装置001
002ソフトウェア002
003入力値制約条件003
004検査条件
005 検査条件判定結果
0011 制約条件付きSSA形式変換部
0012 制約条件付き数値最適化ソルバ用制約形式変換部
0013 制約条件付き数値最適化ソルバ
0014 検査条件判定結果出力部

ページトップへ

この技術を出願した法人

この技術を発明した人物

ページトップへ

関連する挑戦したい社会課題

関連する公募課題

ページトップへ

技術視点だけで見ていませんか?

この技術の活用可能性がある分野

分野別動向を把握したい方- 事業化視点で見る -

ページトップへ

おススメ サービス

おススメ astavisionコンテンツ

新着 最近 公開された関連が強い技術

この 技術と関連性が強い人物

関連性が強い人物一覧

この 技術と関連する社会課題

関連する挑戦したい社会課題一覧

この 技術と関連する公募課題

関連する公募課題一覧

astavision 新着記事

サイト情報について

本サービスは、国が公開している情報(公開特許公報、特許整理標準化データ等)を元に構成されています。出典元のデータには一部間違いやノイズがあり、情報の正確さについては保証致しかねます。また一時的に、各データの収録範囲や更新周期によって、一部の情報が正しく表示されないことがございます。当サイトの情報を元にした諸問題、不利益等について当方は何ら責任を負いかねることを予めご承知おきのほど宜しくお願い申し上げます。

主たる情報の出典

特許情報…特許整理標準化データ(XML編)、公開特許公報、特許公報、審決公報、Patent Map Guidance System データ