Business process models are the fundamental models of commercial systems. Therefore the business processes are issue of optimization as well as verification. When a business process has been identified as comparatively good (or optimal) it is of interest if the realization of the system still realizes this process. In this paper we present an approach how to verify such realizations. As application system we use the e-commerce system Intershop Enfinity which provides an executable process model: the Pipeline Model. These Pipeline Models have to be transferred to formal automata models which then may be checked. As tools to check we use model checkers.