Pattern based property specification and verification for service composition

Service composition is becoming the dominant paradigm for developing Web service applications. It is important to ensure that a service composition comply with the requirements for the application. A rigorous compliance checking approach usually needs the requirements being specified in properties specification formalisms like temporal logics, which are difficult for ordinary software practitioners to write. In this paper, we propose a property pattern based specification language PROPOLS and use it to verify BPEL service composition schemas. PROPOLS is easy to understand and use, yet is formally based. It builds on Dwyer et al's property pattern system and extends it with the logical composition of patterns to accommodate the specification of complex requirements. PROPOLS is encoded in OWL to facilitate the sharing and reuse of domain knowledge. A Finite State Automata based implementation for the verification of BPEL schemas against PROPOLS properties is also discussed.