A major problem in modelling and subsequent simulation of process-oriented systems (ProC/B models), is the functional correctness of the model. Therefore a model should be first analysed for its functional correctness before it is analysed by simulation. Petri nets are well suited for model based and state based functional analysis, but are often not adequate or not used for the specification of process models. We present in this paper a transformer for an automatic mapping from ProC/B models onto PNs. The resulting PN-models can be analysed with PN-algorithms and the results from the PN-analysis can be interpreted at the ProC/B level.