Testing and Verification of Service Compositions

• Author / Creator

  Khaled, Adel

• 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.

• Subjects / Keywords

  • WS-CDL
  • WS-BPEL
  • Testing
  • SOA

• Graduation date

  Spring 2016

• Type of Item

  Thesis

• Degree

  Master of Science

• DOI

  https://doi.org/10.7939/R34M91J85

• License

  This thesis is made available by the University of Alberta Libraries with permission of the copyright owner solely for non-commercial purposes. This thesis, or any portion thereof, may not otherwise be copied or reproduced without the written consent of the copyright owner, except to the extent permitted by Canadian copyright law.