||Web services are the most widely implemented paradigm of service oriented architecture enabling E-business today. In this architecture higher level execution languages facilitate composition and orchestration of web services enabling the creation of business processes. Practice shows that correcting errors in early phases of software development can save time in the later phases. In order to provide error-free interaction of web services between two communicating business partners we provide a method of checking the adherence of two business processes speci_ed in BPEL. This is achieved by checking whether a speci_cation or part of that speci_cation is erroneous compared to the other peer involved in the communication scheme as we derive an inclusion checking algorithm. The inclusion checking and conversion of BPEL to the Abstract BPEL speci_cation is achieved with the use of existing automata theory combined in a particular way. The abstract speci_cation constrains the BPEL speci_cation by exposing behavioral aspects of the functionality of the peers involved in the business process. We provide formal proof and evidence that our inclusion check is conceptually correct and that both approaches are feasible. We provide a proprietary software as proof of concept for the realizability of both the Abstract BPEL speci_cation, the inclusion checking algorithm and as we discuss the implementation and the steps involved the construction of these approaches enabling the automated adherence checking of two BPEL speci_cations.