Extension of an Executable Formal Model of BPEL to Permit Comprehensive Validation

The Business Process Execution Language for Web Services (BPEL) is a specification language designed for automating business processes and transactions through Web services between distributed computers. This project presents an executable model for validation of version 1.1 of the BPEL specification by extending a formal model written in Abstract State Machine Language (AsmL). AsmL is a high-level executable formal specification language based on the theory of Abstract State Machines (ASMs). We integrate this model with a particular Abstract Communication Model (ACM) in order to simulate the behaviour of multiple BPEL communication endpoints representing a credit card application process executing on asynchronous communication architectures. These extensions allow further experimental validation with a more comprehensive model in the design phase of system development.