Verification of Context-Dependent Channel-Based Service Models

Abstract. The paradigms of service-oriented computing and modeldriven 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 servicebased 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 analysis.

• Type: Journal
• Year: 2009
• Where: FMCO
• Authors: Natallia Kokash, Christian Krause, Erik P. de Vink
• Keywords: Data-aware Reo Connectors, FMCO 2009, Formal Methods, Reo Coordination Language, Various Behavioral Protocols