特許
J-GLOBAL ID：200903080841628690
反例解析支援装置
発明者：
,
,
出願人/特許権者：
代理人 (2件)：
伊丹 勝
, 田村 和彦
公報種別：公開公報
出願番号（国際出願番号）：特願2007-296713
公開番号（公開出願番号）：特開2009-122992
出願日： 2007年11月15日
公開日（公表日）： 2009年06月04日
要約：
【課題】状態モデルが設計されていれば検証可能であるとともに、反例内に含まれている、状態遷移モデルで発生する問題点、問題候補箇所を抽出して検証作業を行うユーザの反例解読を支援する。【解決手段】モデル検査をした結果、検証条件を満たさなかった状態とイベントの遷移系列である反例を記憶する反例記憶手段と、他状態を検出して発生するイベントである検出イベントと、この検出イベントの発生有無を決定する状態である被検出状態とを対応づけたリストである関連項目リストを記憶する関連項目リスト記憶手段と、反例の中から問題点である可能性のある箇所である問題候補箇所を出力する探索手段とを有し、探索手段は反例に含まれる状態が被検出状態であるか否かを判定し、反例に含まれる状態が被検出状態である場合に、その被検出状態が次の状態に遷移する前に、関連項目リストに対応した検出イベントが発生しているか否かを判定する。【選択図】図5
請求項（抜粋）：
モデル検査を実行して得た検証結果である反例に含まれる問題候補箇所を出力する反例解析支援装置であって、
モデル検査をした結果、検証条件を満たさなかった状態とイベントの遷移系列である反例を記憶する反例記憶手段と、
他状態に相関のある項目のリストであって、他状態を検出して発生するイベントである検出イベントと、この検出イベントの発生有無を決定する状態である被検出状態とを対応づけたリストである関連項目リストを記憶する関連項目リスト記憶手段と、
前記反例と、前記関連項目リストを用いて、反例の中から問題点である可能性のある箇所である問題候補箇所を出力する探索手段と
を有し、
前記探索手段は、
前記反例に含まれる状態が前記被検出状態であるか否かを判定し、
前記反例に含まれる状態が被検出状態である場合に、その被検出状態が次の状態に遷移する前に、関連項目リストに対応した検出イベントが発生しているか否かを判定し、その検出イベントが発生していないと判定した場合には、問題候補箇所の出力を行う
ことを特徴とする反例解析支援装置。
IPC (1件)：
FI (1件)：
Fターム (2件)：
引用特許：
引用文献：
前のページに戻る
