Binary Activity Chain Modes for Compositional Web Service and Its Compliance Verification

摘要

requirement-driven behavior verification forcompositional Web service is one of hot research issues forWeb computing. Modeling and analysis of the behaviorrequirements of compositional Web service plays animportant role in behavioral verification. Traditionalmethods are expressing requirements as LTL like logicspecifications which are based on activities or as MSC likegraph forms which are based scenarios. In this paper, wepropose the concept of behavior specification based onactivity chain in which its atomic granularity is betweenactivity and scenario. Four behavioral modes such as chainexistence mode, chain absence mode, chain preconditionmode and chain response mode are adopted to express usualrequirement specifications. Encode them on LabeledTransition System LTS and then give them operationsemantics. Check compositional Web services based on LTScorresponds with behavior modes or not. Give the sufficient,necessary condition and algorithm for checking.