| 摘要 |
PURPOSE:To attain logical verification even to a part of a protocol as well whose signal number is infinite by discriminating it as infinite overflow when the system state having the increase signal series of the signal state of the same channel appears so as to stop an extension. CONSTITUTION:A block 8 detects the state that the number of signals stored on a channel between processes is infinite, that is infinite overflow. The L value of state 0.1 of the process 1 is 1.0 and an unprocessed signal series of channels 1.2 are 1.0, 2.0. The L value of the state 0.9 of the process 1 is 1.5 and the unprocessed signals series of the channel 1.2 are 1.3, 2.3, 1.4, 2.4, 1.5, 2.4. Thus, after 0.9, the state transition series is repeated and the signal 1.2 is stored, then it is discriminated as the infinite overflow. Similarly, the state 0.7 of the process 2 is marked by the type 3. Thus, acyclic state extension to the protocol is stopped.
|
