Alloy-based verification of Web service composition

Abstract

Service composition was the core problem of service computing,the validity and reliability of service composition had become the premise of service execution.A method was presented which utilizes the finite state machine (FSM)to model the business process’s state transitions,and described the required properties with Alloy language.Then,Alloy model was used to formalize the service FSM and the required properties of the system.Finally,Alloy Analyzer was used to verify the model that whether the required properties were satisfied.It is shown that the method of Alloy-based verification of the service composition is of good feasibility.

Keywords

• Web service;service composition;finite state machine;Alloy;verification