摘要
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.
基金
国家自然科学基金，国家重点基础研究发展计划(973计划)，中国科学院软件研究所资助项目
