PZ nets - a formal method integrating Petri nets with Z

In this paper, a formal method (called PZ nets) for specifying concurrent a nd distributed systems is presented. PZ nets integrate two well-known exist ing formal methods Petri nets and Z such that Petri nets are used to specif y the overall structure, control flows, causal relation, and dynamic behavi or of a system; and Z is used to define tokens, labels and constrains of th e system. The essence, benefits, and problems of the integration art: discu ssed. A set of heuristics and transformations to develop PZ nets and a tech nique to analyze PZ nets are proposed and demonstrated through a well-known example. (C) 2001 Elsevier Science B.V. All rights reserved.