Beginning with a bounded (safe), live, or reversible Petri net as a first-level net model for a system, Petri nets are synthesized by first refining operation places through basic design modules in top-down modular ways, then adding nonshared resource places stepwise, and finally adding shared resource places step by step in a bottom-up manner. Refinement theory is extended to include reversibility of Petri nets. Parallel and sequential mutual exclusions are used to model shared resources. Design of the first-level Petri nets is discussed, and two basic kinds of Petri nets, choice-free and choice-synchronization, are given to cope with different types of manufacturing systems. The major advantages of the method are that the modeling details can be introduced in incremental ways such that complexity can be handled, and the important properties of the resulting Petri net are guaranteed so that costly mathematical analysis for boundedness, liveness, and reversibility can be avoided. A manufacturing system consisting of four machines, one assembly cell, two shared robots, and two buffers is used to illustrate the design methodology.< >