@inproceedings{1464f6ef1fdf417491255c06d0152522,
title = "Verification of context-dependent channel-based service models",
abstract = "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. Fulltext Preview",
author = "N. Kokash and C. Krause and \{Vink, de\}, E.P.",
year = "2010",
doi = "10.1007/978-3-642-17071-3\_2",
language = "English",
isbn = "978-3-642-17070-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "21--40",
editor = "\{Boer, de\}, F.S. and M.M. Bonsangue and S. Hallerstede and M. Leuschel",
booktitle = "Formal Methods for Components and Objects (FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers)",
address = "Germany",
}