Verification of Context-Dependent Channel-Based Service Models
N. Kokash, C. Krause & E.P. de Vink

The paradigms of service-oriented computing and model-driven
development are becoming of increasing importance in the field of
software engineering. According to these paradigms, new systems are
composed with added value from existing stand-alone services to
support business processes across organizations. Services comprising a
system but originating from various sources need to be
coordinated. The Reo coordination language is a state-of-the-art tool
supported approach to channel-based coordination. Reo introduces
various types of channels which can be composed to build complex
connectors to represent various behavioral protocols. This makes Reo
suitable for the modeling of service-based business processes. In
previous work we presented a framework for model checking data-aware
Reo connectors using the mCRL2 toolset. In this paper, we extend this
result with a proof of correctness, evaluation of optimization
techniques, and support for context-sensitive time-aware analysis.