Temporal colored Petri nets, an extension of temporal Petri nets, areintroduced in this paper. It can distinguish the personality of individuals (tokens), describeclearly the causal and temporal relationships between ...Temporal colored Petri nets, an extension of temporal Petri nets, areintroduced in this paper. It can distinguish the personality of individuals (tokens), describeclearly the causal and temporal relationships between events in concurrent systems, and representelegantly certain fundamental properties of concurrent systems, such as eventuality and fairness.The use of this method is illustrated with an example of modeling and formal verification of anonline stock trading system. The functional correctness of the modeled system is formally verifiedbased on the temporal colored Petri net model and temporal assertions. Also, some main properties ofthe system are analyzed. It has been demonstrated sufficiently that temporal colored Petri nets canverify efficiently some time-related properties of concurrent systems, and provide both the powerof dynamic representation graphically and the function of logical inference formally. Finally,future work is described.展开更多
文摘Temporal colored Petri nets, an extension of temporal Petri nets, areintroduced in this paper. It can distinguish the personality of individuals (tokens), describeclearly the causal and temporal relationships between events in concurrent systems, and representelegantly certain fundamental properties of concurrent systems, such as eventuality and fairness.The use of this method is illustrated with an example of modeling and formal verification of anonline stock trading system. The functional correctness of the modeled system is formally verifiedbased on the temporal colored Petri net model and temporal assertions. Also, some main properties ofthe system are analyzed. It has been demonstrated sufficiently that temporal colored Petri nets canverify efficiently some time-related properties of concurrent systems, and provide both the powerof dynamic representation graphically and the function of logical inference formally. Finally,future work is described.
