This paper presents the applications of several property-preserving Petri net process algebras (PPPA) to the specification and verification of manufacturing system design. It illustrates the applications by designing a Manufacturing System (MS) with componentbased approach. PPPA handles the following three problems: 1) Integrating the primitive modules by using composite operators to create the final model; 2) Handling resource sharing by using place merging operators; and 3) Specifying the machining and/or assembly operations by using place refinement operators. Among other features, PPPA does not need to verify composite components because all the operators preserve many properties. Hence, if the primitive modules satisfy the desirable properties, each of the composite components, including the system itself, also satisfies these properties.