1. A system for verifying operation of a target system to be inspected, the system comprising: a binary-tree generating unit; and a matching unit; wherein the binary-tree generating unit obtains information about a functional specification of the target system and generates one or more binary trees that associate (1) one or more states that can occur in the target system with respective nodes and (2) state transitions of objects constituting the target system and interactions between the objects with connection relationships between the nodes; and wherein the matching unit receives an event sequence in an application model of the target system obtained in response to the operation of the target system to match the event sequence against the binary trees generated by the binary-tree generating unit.