Centered on data abstraction and encapsulation, objectoriented technologies have been widely accepted in software industry in the past decade However, existing object technologies lack precise semantics, which makes them hard to analyze In this paper, a group of patterns is presented to formalize object-oriented systems with PZ nets - a formal integration of Petri nets and Z language These patterns use Petri nets to depict the overall system structure and control flows, class structures and collaborations, and dynamic behavior, and use Z to define the underlying specification of Petri nets.
