(57)【要約】      （修正有）【課題】モデル検査において、反例になる場合に特徴的な状態遷移を反例原因として特定する。【解決手段】モデル検査器からモデル検査の結果の全てをログとして入力し、状態遷移モデルが満たすべき性質を記述した検査式が満たされない場合の状態遷移の実行列を表す反例と判定された場合の実行列である反例ログと、反例と判定されなかった場合の実行列である非反例ログを区別して出力し（Ｓ２１）、反例ログに登場しないノード、反例ログに登場するノード、反例ログの最後の行に対応するノードの３種のノードを持つグラフを生成し（Ｓ２２）、反例ログの最後の行に対応するノードから辿ってきたノード以外に反例ログに登場しないノードへのエッジが存在するノードを分岐を持つノードとし、分岐を持つノードから反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因として特定する（Ｓ２３）。【選択図】図２
2016076188.tif 000002
【特許請求の範囲】
【請求項１】
モデル検査器からモデル検査の結果の全てをログとして入力し、状態遷移モデルが満たすべき性質を記述した検査式が満たされない場合の状態遷移の実行列を表す反例と判定された場合の実行列である反例ログと、反例と判定されなかった場合の実行列である非反例ログを区別して出力するログ出力部と、
前記反例ログおよび前記非反例ログの情報を取得し、前記反例ログに登場しないノード、前記反例ログに登場するノード、前記反例ログの最後の行に対応するノードの３種のノードを持つグラフを生成するグラフ生成部と、
前記グラフを取得し、前記反例ログの最後の行に対応するノードから辿ってきたノード以外に前記反例ログに登場しないノードへのエッジが存在するノードを分岐を持つノードとし、前記分岐を持つノードから前記反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因として特定する原因解析部とを、
備える反例原因解析装置。
【請求項２】
前記ログ出力部から全ての反例ログを取得して格納する反例ログ格納部と、前記ログ出力部から全ての非反例ログを取得して格納する非反例ログ格納部と、前記グラフ生成部で生成されたグラフを格納するグラフ格納部と、前記原因解析部で解析された反例の原因を格納する反例原因格納部とを備える請求項１に記載の反例原因解析装置。
【請求項３】
前記反例ログおよび前記非反例ログには、状態遷移が起きた時の状態、状態遷移のきっかけとなったイベントおよび状態遷移に伴って実行されたアクションの情報が、検査した状態遷移の順に記録される請求項１又は請求項２に記載の反例原因解析装置。
【請求項４】
前記状態遷移に伴って実行されたアクションの情報は、状態遷移に伴うグローバル変数あるいはローカル変数の値の更新状況を表すアクションの結果の情報である請求項３に記載の反例原因解析装置。
【請求項５】
前記グラフ生成部によって生成される前記グラフは、前記反例ログおよび前記非反例ログに記録された状態遷移の順序に沿って、前記ノード間にエッジが引かれる請求項１乃至請求項４のいずれか1項に記載の反例原因解析装置。
【請求項６】
前記グラフ生成部における前記グラフの生成では、状態遷移が起きた時の状態、状態遷移のきっかけとなったイベントおよび状態遷移に伴って実行されたアクションの情報が全て一致する場合に同一のノードと判定し、前記同一のノードが存在する場合には、前記同一のノードに、ノードの種別を設定する請求項５に記載の反例原因解析装置。
【請求項７】
前記グラフ生成部における前記ノードの種別の決定は、
前記ノードの種別を追加する時点で、読み込んだログが前記非反例ログの場合は、前記反例ログに登場しないノードとし、
読み込んだログが前記反例ログの場合は、前記反例ログに登場するノードとし、
前記反例ログの最後の行に相当するノードは、前記反例ログの最後の行に対応するノードとする請求項６に記載の反例原因解析装置。
【請求項８】
前記同一のノードがある場合は、前記反例ログの最後の行に対応するノードの方が前記反例ログに登場するノードより優先し、前記反例ログに登場するノードの方が前記反例ログに登場しないノードより優先する請求項７に記載の反例原因解析装置。
【請求項９】
前記原因解析部における前記反例原因の特定では、前記反例ログの最後の行に対応するノードから、エッジを逆に辿り、辿った先のノードから前記反例ログに登場しないノードへの分岐を探し、前記反例ログに登場しないノードへの分岐が存在しない場合は、更にエッジを逆に辿り、反例に登場しないノードへの分岐がある場合は、分岐を持つノードから前記反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを原因とする請求項１乃至請求項８のいずれか１項に記載の反例原因解析装置。
【請求項１０】
前記反例原因の特定で、解析中のノードから前記反例ログに登場するノードへのエッジが複数存在する場合には、現在解析中のノードを再開ノードとして、一旦、保持しておき、全てのルート探索を行う請求項９に記載の反例原因解析装置。
【請求項１１】
モデル検査器で検査したモデル検査の結果に基づいて、反例原因の解析を行う反例原因解析装置に、
前記モデル検査の結果の全てをログとして入力し、状態遷移モデルが満たすべき性質を記述した検査式が満たされない場合の状態遷移の実行列を表す反例と判定された場合の実行列である反例ログと、反例と判定されなかった場合の実行列である非反例ログを区別して出力する機能と、
前記反例ログおよび前記非反例ログの情報を取得し、前記反例ログに登場しないノード、前記反例ログに登場するノード、前記反例ログの最後の行に対応するノードの３種のノードを持つグラフを生成する機能と、
前記グラフを取得し、前記反例ログの最後の行に対応するノードから辿ってきたノード以外に前記反例ログに登場しないノードへのエッジが存在するノードを分岐を持つノードとし、前記分岐を持つノードから前記反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因として特定する機能とを、
実現させるための反例原因解析プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、反例原因解析装置および反例原因解析プログラムに関する。
【背景技術】
【０００２】
モデル検査器は、検査対象の振る舞いを記述した状態遷移モデルと、状態遷移モデルが満たすべき性質を記述した検査式の２つを入力とし、状態遷移モデルが取り得る状態を網羅的に探索して検査式を満たさない状態の有無を検査する。
【０００３】
モデル検査器は、検査式を満たさない状態を発見した場合、その状態に至るまでの状態遷移の実行列を反例として出力する。
【０００４】
モデル検査器が出力する反例には状態遷移の実行列のみが記述されているため、反例の原因を特定するためには、人手で反例の内容を解析する必要がある。
【０００５】
人手で反例を解析して原因を特定するには、検査対象に対する十分な理解と解析作業に対する経験とノウハウが必要なため、モデル検査にかかるコストを増大させているという問題があった。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２０１０−２０５０６６号公報
【特許文献２】特開２０１３−２０６３１０号公報
【非特許文献】
【０００７】
【非特許文献１】電子情報通信学会  知能ソフトウェア工学研究会（ＫＢＳＥ）２０１３−７９  「モデル検査における反例解析容易化支援」青木善貴・松浦佐江子
【発明の概要】
【発明が解決しようとする課題】
【０００８】
本発明が解決しようとする課題は、モデル検査において、人手によらず、反例になる場合に特徴的な状態遷移を反例原因として特定する反例原因解析装置および反例原因解析プログラムを提供することである。
【課題を解決するための手段】
【０００９】
実施形態の反例原因解析装置は、モデル検査器からモデル検査の結果の全てをログとして入力し、状態遷移モデルが満たすべき性質を記述した検査式が満たされない場合の状態遷移の実行列を表す反例と判定された場合の実行列である反例ログと、反例と判定されなかった場合の実行列である非反例ログを区別して出力するログ出力部と、前記反例ログおよび前記非反例ログの情報を取得し、前記反例ログに登場しないノード、前記反例ログに登場するノード、前記反例ログの最後の行に対応するノードの３種のノードを持つグラフを生成するグラフ生成部と、前記グラフを取得し、前記反例ログの最後の行に対応するノードから辿ってきたノード以外に前記反例ログに登場しないノードへのエッジが存在するノードを分岐を持つノードとし、前記分岐を持つノードから前記反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因として特定する原因解析部とを、備える。
【図面の簡単な説明】
【００１０】
【図１】本発明の実施形態に係る反例原因解析装置の概略構成を示すブロック図である。
【図２】実施形態に係る反例原因解析装置における反例原因の解析処理の流れを示すフローチャートである。
【図３】反例ログと非反例ログの出力処理の流れを示すフローチャートである。
【図４】出力されるログに含まれる情報を説明する図である。
【図５】モデル検査器SPINによる出力ログの一例を示す図である。
【図６】グラフの生成処理の流れを示すフローチャートである。
【図７】ノードの種別の決定処理の流れを示すフローチャートである。
【図８】図７に示したログについてノードの種別決定を実行した一例を示す図である。
【図９】グラフのデータ構造を説明する図である。
【図１０】生成されたグラフの一例を示す図である。
【図１１】反例原因の特定を説明する図である。
【図１２】解析中のノードから反例ログに登場するノードへのエッジが複数存在する場合の反例原因の特定処理の流れを示すフローチャートである。
【図１３】特定された反例原因の一例を示す図である。
【発明を実施するための形態】
【００１１】
以下、本発明の一実施の形態について、図面を参照して説明する。尚、各図において同一箇所については同一の符号を付すとともに、重複した説明は省略する。
【００１２】
まず、本実施形態で用いる主要な用語について説明する。
【００１３】
「モデル検査」とは、状態遷移モデルを対象として、状態遷移モデルが検査式で表された仕様を満足するかを検証する手法をいう。動作仕様がとりうる全ての状態を網羅的に探索し、検査式に反する不適合が発生するか否かの検査をいう。
【００１４】
「状態遷移モデル」とは、状態、イベント、遷移、アクションによって記述されるモデルであって、表現形式としては、状態遷移図や状態遷移表がある。
【００１５】
「検査式」とは、モデル検査の検査対象が満たすべき性質を表現した論理式をいう。線形時相論理、計算木論理に代表される時相論理に基づいて記述する。
【００１６】
「反例」とは、検査式が満たされない場合の状態遷移の実行列をいう。
【００１７】
「反例原因」とは、反例の中で、検査式を満たさないことを特定しうる状態遷移をいう。
【００１８】
状態遷移モデルは、所定のモデル記述言語によってモデル検査プログラム（モデルデータ）として記述することが可能であり、システムの仕様が所定の検査条件を満たすか否かを判定するため、このモデル検査プログラムが検査対象としてモデル検査器に入力される。
【００１９】
モデル検査器では、モデル検査プログラムが取りうる総ての状態遷移の組み合わせに対して、検査式を満たすか否かを判定する。検査式を満たさない状態が発見された場合は、その状態に至るまでの状態遷移の実行列を、反例としてする。また、その状態へ至る過程もログデータとして出力される。
【００２０】
本実施形態においては、反例と判定された場合の実行列を反例ログとし、反例と判定されなかった場合の実行列を非反例ログとし、これら反例ログ、非反例ログに記録された変数の値の組、状態、イベントから成る情報によって、反例ログに登場しないノード、反例ログに登場するノード、反例ログの最後の行に対応するノードを持つグラフを生成し、該グラフから、特定のノードを反例原因として抽出する。
【００２１】
図１は、本発明の実施形態に係る反例原因解析装置の概略構成を示すブロック図である。この装置は汎用のコンピュータ（例えばパーソナルコンピュータ（ＰＣ）等）と、同コンピュータ上で動作するソフトウェアとを用いて実現される。コンピュータとしては、ＣＡＤ（Computer Aided Design）やＣＡＥ（Computer Aided Engineering）に好適なエンジニアリングワークステーション（ＥＷＳ）等も含む。本実施形態はこのようなコンピュータに、反例と判定された場合の実行列である反例ログと、反例と判定されなかった場合の実行列である非反例ログに基づいて、反例ログに登場しないノード、反例ログに登場するノード、反例ログの最後の行に対応するノードを持つグラフを生成し、該グラフから特定のノードを反例原因として抽出するプログラムとして実施することもできる。
【００２２】
図１に示すように、本実施形態に係る反例原因解析装置１は、主として、ログ出力部１１、グラフ生成部１２、原因解析部１３、反例ログ格納部１４、非反例ログ格納部１５、グラフ格納部１６、反例原因格納部１７から構成されている。
【００２３】
ログ出力部１１は、モデル検査器からモデル検査の結果の全てを入力し、検査式を満たさずに反例と判定された場合の実行列である反例ログと、反例と判定されなかった場合の実行列である非反例ログを区別して出力する。反例ログ、非反例ログには、状態遷移が起きた時の“状態”、状態遷移のきっかけとなった“イベント”および状態遷移に伴って実行された“アクションの結果”の情報が、状態遷移の順に記録される。
【００２４】
グラフ生成部１２は、ログ出力部１１から反例ログおよび非反例ログの情報を取得し、“反例ログに登場しないノード”、“反例ログに登場するノード”、“反例ログの最後の行に対応するノード”の３種のノードを持つグラフを生成する。生成されるグラフにおいては、各ログに記録された状態遷移の順序に沿って、各ノード間にエッジが引かれる。
【００２５】
原因解析部１３は、グラフ生成部１２で生成されたグラフを取得し、反例ログの最後の行に対応するノードから辿ってきたノード以外に反例ログに登場しないノードへのエッジが存在するノードを分岐を持つノードとし、分岐を持つノードから、反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因として特定する。
【００２６】
反例ログ格納部１４は、ログ出力部１１から全ての反例ログを取得して格納する。
【００２７】
非反例ログ格納部１５は、ログ出力部１１から全ての非反例ログを取得して格納する。
【００２８】
グラフ格納部１６は、グラフ生成部１２で生成されたグラフを格納する。
【００２９】
反例原因格納部１７は、原因解析部１３で解析された反例の原因を格納する。
【００３０】
次に、公知のモデル検査器であるSPINを用い、以上のように構成された反例原因解析装置１における反例原因の解析処理の流れについて説明する。
【００３１】
図２は、実施形態に係る反例原因解析装置１における反例原因の解析処理の流れを示すフローチャートである。ここでは、解析処理の概要を述べ、各処理の詳細は後述する。
【００３２】
まず、モデル検査器SPINに対して、ログ出力方法を反例ログと非反例ログとに分けて出力するように設定してモデル検査を実行し、反例と判定された場合の実行列である反例ログと反例と判定されなかった場合の実行列である非反例ログを出力させる（ステップＳ２１）。
【００３３】
次いで、これら反例ログ、非反例ログに記録された変数の値の組、状態、イベントから成る情報によって、反例ログに登場しないノード、反例ログに登場するノード、反例ログの最後の行に対応するノードを持つグラフを生成する（ステップＳ２２）。
【００３４】
次に、生成したグラフの構造から、反例ログの最後の行に対応するノードにつながるノードと反例ログに登場しないノードとの分岐が存在するノードから、反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因として特定（ステップＳ２３）し、解析処理を終了する。
【００３５】
＜反例ログと非反例ログの出力＞
次に、反例ログと非反例ログの出力について詳述する。図３は、反例ログと非反例ログの出力処理の流れを示すフローチャートである。
【００３６】
まず、モデル検査器SPINについて、全ての状態を探索するまで検査を継続させるオプションに設定して、モデル検査を実行する（ステップＳ３１）。
【００３７】
次に、実行可能な状態遷移を行い、遷移先の状態が検査式に違反するかを検査する（ステップＳ３２）。
【００３８】
次いで、遷移先の状態が検査式に違反すると判定されたか否かを判別する（ステップＳ３３）。
【００３９】
遷移先の状態が検査式に違反すると判定された場合（ステップＳ３３でＹｅｓ）には、検査した状態に至るまでの状態遷移を、反例ログとして出力する（ステップＳ３４）。
【００４０】
図４は、出力されるログに含まれる情報を説明する図である。図４に示すように、出力されるログには、状態遷移表に登場する“状態”のいずれであるかを表す情報、状態遷移表に登場する“イベント”のいずれであるかを表す情報、グローバル変数あるいはローカル変数の値がどう更新されたかを表す“アクションの結果”の情報が記述される。記録している変数は、全てのログで共通である。図４に示す例では、状態“１４”で、変数の値が（０，１）の時に、発生したイベント“１”が記録される。状態とイベントは、それと識別可能なIDで表現される。また、アクションが実行された結果、変数の値がどう変化したかという実行結果がアクションの結果として記録される。
【００４１】
図５は、モデル検査器SPINによる出力ログの一例を示す図である。図５の１行目には、SPINにおける並行処理の動作主体を示すプロセスＩＤが“０”、処理の中身が“５７４“、変数の値の組が”０，０，０“、状態が”７“、イベントが”０“と記述されている。さらに、８行目から９行目には、状態が、”７“で表される状態から、”４“で表される状態に遷移し、アクションの結果として、変数の値の組が、（０，０，０）から（０，０，１）に更新されたことが記録されている。
【００４２】
一方、遷移先の状態が検査式に違反すると判定されなかった場合（ステップＳ３３でＮｏ）には、検査した状態に至るまでの状態遷移を、非反例ログとして出力する（ステップＳ３５）。非反例ログについても、図４に示すような情報が記述される。
【００４３】
次に、全ての状態を検査したか否かを判別する（ステップＳ３６）。
【００４４】
全ての状態を検査していなければ（ステップＳ３６でＮｏ）ステップＳ３２に戻り、一方、全ての状態を検査していれば（ステップＳ３６でＹｅｓ）、反例ログと非反例ログの出力処理を終了する。
【００４５】
＜グラフの生成＞
次に、グラフの生成について詳述する。図６は、グラフの生成処理の流れを示すフローチャートである。
【００４６】
まず、反例ログ格納部１４または非反例ログ格納部１５から、ログを１つ読み込む（ステップＳ６０１）。
【００４７】
次に、初期ノードを作成して現在のノードに設定する（ステップＳ６０２）。ここで、初期ノードは、全ての値を“−１”にした便宜上のノードである。尚、係る値は、任意に設定することができる。
【００４８】
次いで、読み込んだログから１行分の情報を読み込む（ステップＳ６０３）。尚、ログの１行分を１つのノードとする。
【００４９】
続いて、同一のノードが存在するか否かを判定する（ステップＳ６０４）。ここで、状態、イベント、アクションの結果を表す情報（値）が全て一致する場合のみ、“同一のノード”と判定する。
【００５０】
同一のノードが存在する場合（ステップＳ６０４でＹｅｓ）には、同一のノードを次のノードに設定（ステップＳ６０５）した後、次のノードに、ノードの種別を追加する（ステップＳ６０６）。
【００５１】
一方、同一のノードが存在しない場合（ステップＳ６０４でＮｏ）には、読み込んだ行に対応するノードを追加（ステップＳ６０７）し、追加したノードを次のノードに設定（ステップＳ６０８）した後、次のノードに、ノードの種別を追加する（ステップＳ６０６）。
【００５２】
ノードの種別の決定の詳細については、以下に記すように行う。
【００５３】
＜ノードの種別の決定＞
本実施形態においては、反例ログか非反例ログかによって、ノードの種別を（１）反例ログに登場しないノード、（２）反例ログに登場するノード、（３）反例ログの最後の行に対応するノード、の３種類に分類する。
【００５４】
分類に際しては、以下のような、ルールを定める。
【００５５】
（ａ）ノードの種別を追加する時点で、読み込んだログが非反例ログの場合は、“反例ログに登場しないノード”とする。
【００５６】
（ｂ）読み込んだログが反例ログの場合は、“反例ログに登場するノード”とする。
【００５７】
（ｃ）反例ログの最後の行に相当するノードは、“反例ログの最後の行に対応するノード”とする。
【００５８】
（ｄ）同一のノードがある場合は、“反例ログの最後の行に対応するノード”の方が“反例ログに登場するノード”より優先され、“反例ログに登場するノード”の方が“反例ログに登場しないノード”より優先される。
【００５９】
図７は、ノードの種別の決定処理の流れを示すフローチャートである。
【００６０】
まず、読み込んだログが反例ログか否かを判定する（ステップＳ７１）。
【００６１】
読み込んだログが反例ログであれば（ステップＳ７１でＹｅｓ）、次に、読み込んだ行が最後の行か否かを判定する（ステップＳ７２）。
【００６２】
読み込んだ行が最後の行であれば（ステップＳ７２でＹｅｓ）、次のノードの種別を“反例ログの最後の行に対応するノード”に分類（ステップＳ７３）し、ノードの種別の決定処理を終了する。
【００６３】
一方、読み込んだ行が最後の行でなければ（ステップＳ７２でＮｏ）、次のノードが既に“反例ログの最後の行に対応するノード”になっているか否かを判定する（ステップＳ７４）。
【００６４】
“反例ログの最後の行に対応するノード”でなければ（ステップＳ７４でＮｏ）、次のノードの種別を“反例ログに登場するノード”に分類（ステップＳ７５）し、ノードの種別の決定処理を終了する。一方、“反例ログの最後の行に対応するノード”であれば（ステップＳ７４でＹｅｓ）、ノードの種別の決定処理を終了する。
【００６５】
ステップＳ７１でＮｏ、すなわち、読み込んだログが反例ログでなければ、次のノードが追加したノードだったか否かを判定する（ステップＳ７６）。次のノードが追加したノードでなければ（ステップＳ７６でＮｏ）、ノードの種別の決定処理を終了する。
【００６６】
一方、次のノードが追加したノードであれば（ステップＳ７６でＹｅｓ）、次のノードの種別を“反例ログに登場しないノード”に分類（ステップＳ７７）し、ノードの種別の決定処理を終了する。
【００６７】
図８は、図７に示したログについてノードの種別決定を実行した一例を示す図である。図８に示すように、非反例ログは全て「反例ログに登場しないノード」に分類され、反例ログについては、実行した状態遷移の１手乃至１２手のログは「反例ログに登場するノード」に分類され、実行した状態遷移の１３手乃至１６手のログ（０，０，１：４：２３）は、“反例ログの最後の行に対応するノード”に分類されている。
【００６８】
＜グラフの生成−続き＞
次に、現在のノードから次のノードにエッジを追加する（ステップＳ６０９）。図９は、グラフのデータ構造を説明する図である。図９に示すように、ノードは、固有のIDと、ログに記録されているイベント、状態、アクションの結果から成る値をプロパティに持つ。また、ノードの種別を、例えば、判別を容易にする観点からノードに着色して表す場合には、当該色の値をプロパティに持つ。エッジは、ノードの固有のIDで、エッジのソースとターゲットを保持する。
【００６９】
次に、次のノードを現在のノードに設定する（ステップＳ６１０）。
【００７０】
続いて、全ての行を読み込んだか否かを判定する（ステップＳ６１１）。
【００７１】
全ての行を読み込んでなければ（ステップＳ６１１でＮｏ）、ステップＳ６０３に戻り、一方、全ての行を読み込んだならば（ステップＳ６１１でＹｅｓ）、全てのログを読み込んだか否かを判定する（ステップＳ６１２）。
【００７２】
全てのログを読み込んでなければ（ステップＳ６１２でＮｏ）、ステップＳ６０１に戻り、全てのログを読み込んだならば（ステップＳ６１２でＹｅｓ）、グラフの生成処理を終了する。
【００７３】
図１０は、生成されたグラフの一例を示す図である。図１０に示すように、状態遷移の順序に沿って、反例ログに登場しないノード、反例ログに登場するノード、反例ログの最後の行に対応するノードの３種類に分類されたノード間にエッジが引かれている。
【００７４】
＜反例原因の特定（１）＞
次に、以下のような手順によって、グラフ構造から反例原因を特定する。
【００７５】
（１）反例ログの最後の行に対応するノードから、エッジを逆に辿る。
【００７６】
（２）辿った先のノードから反例ログに登場しないノードへの分岐を探す。
【００７７】
ここで、反例ログに登場しないノードへの分岐が存在しない場合は、更にエッジを逆に辿り、反例に登場しないノードへの分岐がある場合は、分岐を持つノードから反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因と判断する。図１１は、反例原因の特定を説明する図である。図１１に示すように、反例ログの最後の行に対応するノードＡから、エッジを逆に辿り、「分岐を持つノード」Ｂ１から１つだけエッジを進めたノードＣ１を反例原因と特定する。上記した図１０に示すグラフの一例においても、ノードＡ、ノードＢ１が示されている。
【００７８】
＜反例原因の特定（２）＞
反例原因の特定処理において、解析中のノードから反例ログに登場するノードへのエッジが複数存在する場合には、辿り得るルートが複数あることから、現在解析中のノードを、“再開ノード”として、一旦、保持しておき、全てのルート探索を行うのが好適である。
【００７９】
図１２は、解析中のノードから反例ログに登場するノードへのエッジが複数存在する場合の反例原因の特定処理の流れを示すフローチャートである。
【００８０】
まず、グラフ中から反例と判定されたノードを探索する（ステップＳ１２０１）。
【００８１】
次に、反例と判定されたノードをターゲットとするエッジをソース側に辿った先のノードを取得する（ステップＳ１２０２）。
【００８２】
次に、得たノードを“解析中ノード”に設定する（ステップＳ１２０３）。解析中ノードは、反例原因の解析をまさに行っているノードを指すポインタの役割を果たすものである。
【００８３】
続いて、反例ログの最後の行に対応するノードから辿ってきたノード以外に、解析中ノードから反例ログに登場しないノードへのエッジが存在するか否かを判定する（ステップＳ１２０４）。すなわち、「分岐を持つノード」であるかは、１つ前の解析中ノード以外に、反例ログに登場しないノードへのエッジが存在するか、によって判定している。上記した図１１において、Ｂ２と記した反例ログに登場しないノードにとって、反例ログの最後の行に対応するノードＡから辿ってきたノードは、左上の反例ログに登場しないノードＣ２になる。ノードＢ２には、ノードＣ２以外にも反例ログに登場しないノードへのエッジ、すなわち、左下の反例ログに登場しないノードへのエッジが存在している。よって、ノードＢ２は、「分岐を持つノード」と判定される。
【００８４】
解析中ノードから反例ログに登場しないノードへのエッジが存在しなければ（ステップＳ１２０４でＮｏ）、次に、解析中ノードへのエッジが複数存在するか否かを判定する（ステップＳ１２０５）。
【００８５】
解析中ノードへのエッジが複数存在するならば（ステップＳ１２０５でＹｅｓ）、解析中ノードを“再開ノード”として記録（ステップＳ１２０６）し、次に、探索していない次のノードを辿る（ステップＳ１２０７）。
【００８６】
一方、解析中ノードへのエッジが複数存在しない場合には（ステップＳ１２０５でＮｏ）、ステップＳ１２０７に移行する。
【００８７】
続いて、得たノードが初期ノードか否かを判定する（ステップＳ１２０８）。
【００８８】
得たノードが初期ノードでなければ（ステップＳ１２０８でＮｏ）、ステップＳ１２０３に移行し、得たノードが初期ノードであれば（ステップＳ１２０８でＹｅｓ）、ステップＳ１２１０に移行する。
【００８９】
上記のステップＳ１２０４でＹｅｓ、すなわち、解析中ノードから反例ログに登場しないノードへのエッジが存在するならば、次に、解析中ノードから反例ログの最後の行に対応するノードに向かって１つだけエッジを進めたノードを反例原因と特定する（ステップＳ１２０９）。
【００９０】
続いて、再開ノードが存在するか否かを判定する（ステップＳ１２１０）。
【００９１】
再開ノードが存在しなければ（ステップＳ１２１０でＮｏ）、全ての反例ログの最後の行に対応するノードを解析したか否かを判定する（ステップＳ１２１１）。
【００９２】
一方、再開ノードが存在するならば（ステップＳ１２１０でＹｅｓ）、再開ノードを解析中ノードと設定（ステップＳ１２１２）し、ステップＳ１２０７に移行する。
【００９３】
全ての反例ログの最後の行に対応するノードを解析していなければ（ステップＳ１２１１でＮｏ）、ステップＳ１２０１に戻り、全ての反例ログの最後の行に対応するノードを解析していれば（ステップＳ１２１１でＹｅｓ）、反例原因の特定処理を終了する。図１１に示す例では、ノードＣ１、Ｃ２が反例原因として特定されることになる。
【００９４】
以上のようにして、特定されたノードが持つプロパティを反例原因として出力する。図１３は、特定された反例原因の一例を示す図である。図１３に示す例では、反例原因は、次の条件が満たされた場合であると判断することができる。
【００９５】
（ａ）変数の値が（０、１、０）で、状態を表す値が“１”の時に、“２４”で表されるイベントが発生することが原因である。
【００９６】
（ｂ）その後、発生したイベント（“２４”で表されるイベント）の結果として、状態を表す値が“７”に更新され、
（ｃ）その後、更に“２４”で表されるイベントが発生し、変数の値が（０、１、１）に、状態を表す変数が“４”に更新される、
という一連の状態遷移によって、検査式を満たさなくなることが確認できる。
【００９７】
以上説明したように、本実施形態によれば、モデル検査において、人手によらず、反例になる場合に特徴的な状態遷移を特定することができる。
【００９８】
本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【符号の説明】
【００９９】
１・・・反例原因解析装置
１１・・・ログ出力部
１２・・・グラフ生成部
１３・・・原因解析部
１４・・・反例ログ格納部
１５・・・非反例ログ格納部
１６・・・グラフ格納部
１７・・・反例原因格納部
【図１】
2016076188.tif 000003
【図２】
2016076188.tif 000004
【図３】
2016076188.tif 000005
【図４】
2016076188.tif 000006
【図５】
2016076188.tif 000007
【図６】
2016076188.tif 000008
【図７】
2016076188.tif 000009
【図８】
2016076188.tif 000010
【図９】
2016076188.tif 000011
【図１０】
2016076188.tif 000012
【図１１】
2016076188.tif 000013
【図１２】
2016076188.tif 000014
【図１３】
2016076188.tif 000015