A Type System for Behavior Consistent Service Substitution in Service Compositions

Service-oriented computing (SOC) requires a flexible service interaction mechanism to facilitate run-time adaptation to dynamic environments. However, the current service interaction mechanism focuses only on the interfaces and static non-functional properties of related services, and ignores the behavior of services, let alone the run-time errors caused by behavior inconsistency. In this paper, a static approach is proposed to study behavior consistent composition and substitution of services in dynamic environments. We first extend the λ calculus with a concurrent expression to describe a service model. Then, a type and effect system is introduced to automatically infer conservative approximations of a service behavior represented by concurrent behavior expressions arising at runtime. Finally, by using the Coq proof assistant we mechanized formalization and the proof of type safety, which can guarantee that the type and effect system discovers a substitute service for each "unavailable service" that meets the constraints of behavior consistency.