Formal semantics analysis of data flow and control flow for web composition transactions

Web composition business process is the choreography of atomic activities and composition activities. To construct data flow and control flow, atomic activities and structured activities such as sequence, switch, flow and loop are formally described based on Petri net analysis. Considering the failure and compensation of composition transaction, compensation activities and sequence that handlers were triggered in nesting levels are analyzed according to scope, interface dependency and compensation dependency. Mapping of compensation context and activities and scopes in structured activities is discussed. A novel perspective of formalization of data flow and control flow for web services choreography is proposed.