The paradigms of service-oriented computing and model-driven development are becoming of increasing importance in the eld 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 computer 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.
Additional Metadata
ACM Design Tools and Techniques (acm D.2.2)
THEME Software (theme 1)
Publisher Springer
Project Compliance-driven Models, Languages and Architectures for Services
Conference International Symposium on Formal Methods for Components and Objects
Citation
Kokash, N, C. (born Köhler, , C.) Krause, ,, & de Vink, E.P. (2010). Verification of Context-Dependent Channel-Based Service Models. In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'09). Springer.