Verification of Communication Protocols in Web Services: Model-Checking Service Compositions

CHAPTER 8

FRAMEWORK FOR MODELING, SIMULATION, AND VERIFICATION OF A BPEL SPECIFICATION

In previous chapters we described methods for reducing the time and memory requirements for model checking. These methods offer incentives to use formal methods of verifying service-oriented architecture (SOA)–based applications. These chapters have also emphasized the ingenuity of formal methods in endorsing the safety and reliability of software systems. Following their widespread use in soft-ware engineering, they are increasingly being adopted for verification of SOA-based applications [14,19,32,33]. This is helping in identifying subtle errors in a Business Process Execution Language (BPEL) specification, the de facto industry standard for service composition. Such errors would often elude conventional simulation and testing techniques.

SOA-based applications have assumed widespread acceptance, owing to their agility, maintainability, and modularity. However, the safety and reliability of such loosely coupled systems depend entirely on the precision of service descriptions. Consequently, any implicit assumption or unforeseen usage scenarios can lead to catastrophic fiascos. This is exacerbated further by the overlapping constructs and inconsistencies in BPEL.

Conventional techniques cannot be used to verify an SOA-based application because (1) the fault, if any, is related primarily to the business logic for service composition rather than the source code or implementation of underlying ...