Methods and systems are provided for automatically generating an accurate model of communications processes between disparate computing systems that may be analyzed in an efficient manner for error detection in web services systems. Business Process Execution Language for Web Services (BPEL) descriptions are automatically generated for the BPEL-based executable processes utilized by each communicating computing system in a given web services system. The BPEL abstract process descriptions for each communicating computing system are translated into a combined process model according to a suitable modeling language. The process model is tested by a model checking software application. Communications errors between the disparate computing systems are detected by automatically testing the combined process model according to a variety of potential communications scenarios.