| 摘要 |
A counter example analysis support apparatus includes a counter example storage storing the counter example being a transition sequence of state and event that has not satisfied a verification condition as a result of the model checking; comprising: a related item list storage storing a related item list being a list associating a detection event, which is an event for detecting and generating the other-state, and a detected state, which is a state for determining the existence of the generation of the detection event; and a searching unit outputting a possible problem part from the counter example, wherein the searching unit determines whether a state included in the counter example is the detected state, and if the state included in the counter example is the detected state, determines whether a detection event corresponding to the related item list is generated before the detected state transits to a next state.
|
