CAUSE OF COUNTEREXAMPLE ANALYSIS DEVICE AND CAUSE OF COUNTEREXAMPLE ANALYSIS PROGRAM

摘要

PROBLEM TO BE SOLVED: To specify a characteristic state transition as the cause of counterexample in the case of a counterexample in model inspection.SOLUTION: All of results of model inspection from a model checker are inputted as logs, and a counterexample log that is an execution example when determined to be a counterexample representing the execution example of a state transition where an inspection formula is not satisfied in which the properties that a state transition model must satisfy is described and a non-counterexample log that is an execution example when determined not to be a counterexample are outputted separately from each other (S21). A graph is generated that has three kinds of nodes: a node not appearing in the counterexample log, a node appearing in the counterexample log, and a node corresponding to the last line of the counterexample log (S22). Assuming that a node in which there exists an edge to the node not appearing in the counterexample log other than nodes traced from the node corresponding to the last line of the counterexample log to be a node having a branch, a node advanced one edge from the node having the branch toward the node corresponding to the last line of the counterexample log is specified as the cause of counterexample (S23).SELECTED DRAWING: Figure 2