PZ nets - a formal method integrating Petri nets with Z
Article
He, X. (2001). PZ nets - a formal method integrating Petri nets with Z
. INFORMATION AND SOFTWARE TECHNOLOGY, 43(1), 1-18. 10.1016/S0950-5849(00)00134-8
He, X. (2001). PZ nets - a formal method integrating Petri nets with Z
. INFORMATION AND SOFTWARE TECHNOLOGY, 43(1), 1-18. 10.1016/S0950-5849(00)00134-8
In this paper, a formal method (called PZ nets) for specifying concurrent and distributed systems is presented. PZ nets integrate two well-known existing formal methods Petri nets and Z such that Petri nets are used to specify the overall structure, control flows, causal relation, and dynamic behavior of a system; and Z is used to define tokens, labels and constrains of the system. The essence, benefits, and problems of the integration are discussed. A set of heuristics and transformations to develop PZ nets and a technique to analyze PZ nets are proposed and demonstrated through a well-known example.
