Verification of context-dependent channel-based service models

N. Kokash, C. Krause, E.P. Vink, de

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

15 Citations (Scopus)


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
Original languageEnglish
Title of host publicationFormal Methods for Components and Objects (FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers)
EditorsF.S. Boer, de, M.M. Bonsangue, S. Hallerstede, M. Leuschel
Place of PublicationBerlin
ISBN (Print)978-3-642-17070-6
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Verification of context-dependent channel-based service models'. Together they form a unique fingerprint.

Cite this