The Business Process Execution Language for Web Services provides a powerful technology to aggregate encapsulated functionalities and define high-value Web services - backed by various development and runtime environments of major software companies. Nevertheless, modeling and composing BPEL processes is still a complicated, time and money consuming, and errorprone activity. Formal methods like Petri nets enable the effective analysis of one single BPEL process as well as the comparison of multiple given BPEL models, and the generation of a BPEL model out of another. The current paper presents an prototypically implemented analysis framework that integrates those methods into IBM?s business integration tools. The value of such a framework is illustrated by analyzing behavioral compatibility between BPEL processes, one of the most crucial properties in real-world B2B scenarios.