ON-THE-FLY MODEL OF SYSTEM FOR EXECUTING CHECKING THROUGH THE USE OF REDUCED PARTIAL ORDER STATE SPACE

摘要

PURPOSE: To provide an on-the-fly verification system for adopting information which can statistically be used for reducing the size of a state space requested for verifying the active characteristic and the safety characteristic of a target system constituted of an asynchronous communication process. ;CONSTITUTION: The verification system generates a verifier 111 from the description 103 of the target system which is to be verified and the specification of the characteristic 107. The verifier 111 models the target system as one set of finite state machines, constitutes a state space 19 containing the state of the target system and the graph of a node 121 expressing the shift between the states and verifies the characteristics by using the state space 119. The size of the state space 119 is reduced by dividing shift from the prescribed node into groups for respective processes and deciding which group of the shift is contained in the state space and which is to be removed from the state space by using information from the description 103 and the specification. The state space reduction method does not increase the size of the state space but it occasionally reduces it by the scale of the number of digits.;COPYRIGHT: (C)1995,JPO