Testing and Verification of Service Compositions
Khaled, Adel · ERA: Education and Research Archive (University of Alberta) · 2016
Service Oriented Architecture (SOA) delivers on the promise of dynamic applications that are better aligned with business goals. Building SOA systems, whether choreography or orchestrated, involve the interaction and collaboration of different parties through service calls. SOA architectural paradigm introduces a set of challenges that make SOA system verification different from conventional software systems. In this research, we explore the opportunities in the area of testing and verification of SOA systems built on top of the two main standards 1) Web Service Choreography Description Language (WS-CDL) and 2) Web Service Business Process Execution Language (WS-BPEL). In this regard, we introduce a formal language based on pi-calculus, Chor-calculus, for the formal modeling and verification of WS-CDL programs. This approach enables the static verification of choreographies using existing pi-calculus model-checker tools and sets the ground for enabling the runtime monitoring of choreographies for behavioral correctness. We validate the calculus for its expressiveness by evaluating the language support for representing workflow, and service interaction, patterns. We demonstrate the use of the HAL toolkit to verify the correctness properties of choreographies. On the other hand, we introduce a set of mutation operators for WS-BPEL and use mutation testing to verify the behavioral correctness of WS-BPEL programs. The fault models can be employed in mutation testing to assess the effectiveness of test suites or measure the accuracy of runtime monitors that are capable of verifying the correctness. We introduce a language to capture the trace behavior of BPEL programs and describe the fault models. We also propose a runtime verification system that consumes the specification language and detects temporal faults.