Abstract:

Building the formal model of composite services is the basis of verification. But in the absence of a unified modeling framework, automatic operations of the modeling process are difficult to realize. We build a services process automata by expanding the deterministic finite automata. It is a finite migratory system which is suitable for describing the process model of OWLS. This work provides a unified framework and a foundation of automatic operations for the formal modeling of composite services. In addition, we divide the compatibility into three grades by analyzing the acceptable locations of the services process automata and the constraints possibly produced during the composition process. So the proposal can be adaptive to verification of composite services with different reliability requirements.

Key words: services composition verification;OWL-S;formal model;services process automata;compatibility analysis