Behavior requirement expression and its satisfiability verification for composite Web services is one of the ongoing issues in service computing. In this paper, the concept of behavior specifications based on activity...Behavior requirement expression and its satisfiability verification for composite Web services is one of the ongoing issues in service computing. In this paper, the concept of behavior specifications based on activity sequence is proposed to express one kind of behavioral requirements for composite Web services. Its basic element is activity sequence. The method to express such behavioral requirements by behavioral modes is presented. Five behavioral modes used in this method are adopted. Through map- ping modes to Labeled Transition Systems （LTSs）, these modes are encoded with exact operation semantics. Then, the sufficient and necessary conditions as well as the checking algorithm for satisfiability of behavioral modes are given. Finally, an example analysis is presented. The result indicates that the behavioral requirements based on activity sequence are more suitable for the case of composite Web service than those based on activity or scenario. The behavioral modes expressions are concise and the satisfiability checking is effective by the given algorithm.展开更多
基金Supported by Guangxi Science Research and Technology Development Program,China (GSRTD 0992006-13)Doctoral Foundation Program of Guangxi University of Technology,China (DFPGUT 11Z05)
文摘Behavior requirement expression and its satisfiability verification for composite Web services is one of the ongoing issues in service computing. In this paper, the concept of behavior specifications based on activity sequence is proposed to express one kind of behavioral requirements for composite Web services. Its basic element is activity sequence. The method to express such behavioral requirements by behavioral modes is presented. Five behavioral modes used in this method are adopted. Through map- ping modes to Labeled Transition Systems （LTSs）, these modes are encoded with exact operation semantics. Then, the sufficient and necessary conditions as well as the checking algorithm for satisfiability of behavioral modes are given. Finally, an example analysis is presented. The result indicates that the behavioral requirements based on activity sequence are more suitable for the case of composite Web service than those based on activity or scenario. The behavioral modes expressions are concise and the satisfiability checking is effective by the given algorithm.
