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 analysis.
|Title of host publication||Formal Methods for Components and Objects (FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers)|
|Editors||F.S. Boer, de, M.M. Bonsangue, S. Hallerstede, M. Leuschel|
|Place of Publication||Berlin|
|Publication status||Published - 2010|
|Name||Lecture Notes in Computer Science|