Pat
J-GLOBAL ID：201603001149258032
プログラム検査装置、ソフトウェア検査装置、SAT制約条件データ、記憶媒体
Inventor：
,
,
,
Applicant, Patent owner：
Agent (3)：
平木 祐輔
, 関谷 三男
, 渡辺 敏章
Gazette classification：公開公報
Application number (International application number)：2014185326
Publication number (International publication number)：2016057969
Application date： Sep. 11, 2014
Publication date： Apr. 21, 2016
Summary：
【課題】検査対象ソフトウェアに対して入力する異常な入力値列をあらかじめ排除することにより、ソフトウェアの挙動を検査するために必要な計算リソースを抑制するプログラム検査装置、ソフトウェア検査装置、SAT制約条件データ、記憶媒体を提供する。【解決手段】プログラム検査装置は、検査対象である動的プログラムの入力値列、内部状態値列、出力値列、及びソフトウェアの要件を記述した検査条件を、充足可能性問題の制約条件として記述し、所望の検査条件を満たす解を探索することにより、検査に適した入力値列を出力値列から逆算的に求める。【選択図】図3
Claim (excerpt)：
入力値にしたがって内部状態値を更新するとともに前記入力値に対応する出力値を出力する処理を実装した動的プログラムを検査するプログラム検査装置であって、
指定した制約条件を充足することができる解を求めることにより前記動的プログラムの前記入力値、前記内部状態値、および前記出力値を検査するSATソルバを備え、
前記SATソルバは、
前記内部状態値を前記動的プログラムに保持させつつ入力値列内の入力値を前記動的プログラムに対して順次引き渡して実行することにより求められる前記動的プログラムの内部状態値列と出力値列を前記入力値列とともに記述した動的プログラム記述、
前記入力値列が満たすべき検査条件、前記内部状態値列が満たすべき検査条件、および前記出力値列が満たすべき検査条件の少なくともいずれかを記述した検査条件記述、
を前記制約条件として受け取り、前記制約条件に違反する前記入力値列、前記制約条件に違反する前記内部状態値列の初期値、および前記制約条件に違反する前記出力値列の少なくともいずれかが存在するか否かを前記解として探索し、前記解が存在しない場合はその旨の処理結果を出力し、前記解が存在する場合はその解に対応する前記入力値列、前記内部状態値列、および前記出力値列を出力する
ことを特徴とするプログラム検査装置。
IPC (2)：
FI (2)：
G06F11/28 340A
, G06F9/06 620M
5B042GB08
, 5B042HH07
, 5B042HH17
, 5B376BB05
, 5B376BC38
, 5B376BC69
, 5B376BC70
, 5B376BC71
