Specification model inspection method and specification model inspection device

摘要

In specification model checking expressed by a transition of plurality of function blocks, whether or not a target value is satisfied is verified with respect to each of the plurality of function blocks. Upon extraction of a function block having a state transition which does not satisfy a target value, the target block is refined corresponding to the state transition, and also, target values of other function blocks are refined corresponding to the target value of the specification model. Under the restriction that the extracted function block violates the target value, if the other function blocks satisfy the refined target values, it is judged that the specification model satisfies the target value.