| 摘要 |
PURPOSE:To enable a protocol designer to execute a protocol verification without necessitating to generate a Petri net by generating automatically an analysis model Petri net which unifies and expresses the relation of the state transition of respective communication program. CONSTITUTION:The verification of a protocol is executed by retrieving whether an undesirable state exists or not in a generated reachable tree. In the course of the generation of the reachable tree, when a newly obtained system state is stored by the format of a node 1000, all the states of the system state are expressed by a bit string. Then, 1 is set for the bit of a place, corresponding to the system state, formed based on a prescribed flow chart, and 0 is set for other bit, and they are encoded. The said state code is converted by an adequate hash function 201, and a correspondence between the state code and the storage place of the node of the reachable tree, corresponding to the said state code, is stored in a hash table 200. After the above-mentioned processing, the system state is retrieved, and the protocol is verified.
|
