A comparison of model checking tools for service oriented architectures.

摘要

Recently most of the research pertaining to Service-Oriented Architecture (SOA) is based on web services and how secure they are in terms of efficiency and effectiveness. This requires validation, verification, and evaluation of web services. Verification and validation should be collaborative when web services from different vendors are integrated together to carry out a coherent task. For this purpose, novel model checking technologies have been devised and applied to web services. "Model Checking" is a promising technique for verification and validation of software systems. WS-BPEL (Business Process Execution Language for Web Services) is an emerging standard language to describe web service composition behavior. The advanced features of BPEL such as concurrency and hierarchy make it challenging to verify BPEL models. Based on all such factors my thesis surveys a few important technologies (tools) for model checking and comparing each of them based on their "functional" and "non-functional" properties. The comparison is based on three case studies (first being the small case, second medium and the third one a large case) where we construct synthetic web service compositions for each case (as there are not many publicly available compositions [1]). The first case study is "Enhanced Loan-Approval Process" and is considered a small case. The second is "Enhanced Purchase Order Process" which is of medium size and the third, and largest is based on a scientific workflow pattern, called the "Service Oriented Architecture Implementing BOINC Workflow" based on BOINC (Berkeley Open Infrastructure Network Computing) architecture.