A Rewriting Based Model for Nondeterministic Composite Web Service System

The network delays, failures and randomization make the composite web service system nondeterministic and difficult to be analyzed. However a probabilistic model can capture and abstract these sources of non-determinism more precisely and enable statistical analysis and simulations. We propose probabilistic rewrite theories as a general semantic framework supporting high level specification of probabilistic systems that can be massively concurrent. With the following two additional assertions, assumption and commitment, probabilistic rewrite theories facilitate reasoning about the composition and verification of services integration. The PMaude, a rewriting methodology based tool in which probabilistic formal modeling and analysis can be used from the earliest phases of nondeterministic system design to uncover many errors and inconsistencies, and to reach high assurance for critical composite web service system.