In: Proceedings of the 7th International Conf. on Software Engineering and Knowledge Engineering (SEKE'95), pages 173-180. June 1995.
Also in: Information and Software Technology, Vol. 43, No. 1, pages 1-18. 2000.
Abstract: 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.
Keywords: PZ nets, Petri nets, Z, formal methods, formal specification, formal verification.
Back to the Petri Nets Bibliography