Type theory based semantic verification for service composition in cloud computing environments

To ensure successful running of service composition in software-as-a-service (SaaS) applications under dynamic cloud computing environments, service semantic verification becomes essentially important and meaningful. Taking advantages from both semantic expression in dependence record types (DRT) and completeness of service description in session types (ST), this paper presents a novel method for service composition verification at semantic level. Based on the characteristics of DRT, an ontology approach is proposed to enrich DRTs semantic description and establish a set of subtyping rules to characterize relationships of transmitted messages among services. As a general service composition description and semantic verification method, message DRT extended multiparty session types (MDRT-MST) are then constructed. A theoretical justification on the main patterns of service composition models is given through the extended reduction rules. As a case study, an online payment system is implemented for evaluating the system performance in practice. Experimental results demonstrate the feasibility and effectiveness of the proposed method in service reduction and verification for the real-world SaaS applications.