Date and Time: Thursday, 14 January 2010, 15:45 - 16:45

Location: HG 6.96

Speaker: Natallia Kokash (CWI)

Title: Translating Reo to mCRL2

Abstract:

Reo is a channel-based coordination language with well-defined semantics that enables a compositional construction of complex connectors from a set of primitive channels. It has been successfully applied to service coordination, business process modeling and mash-up building.

In this talk, I present our approach to modeling and verification of Reo connectors using process specification language mCRL2 and the corresponding model checking toolset. I start from the encoding of Reo in mCRL2 according to its constraint automata semantics, and then discuss several lines of ongoing work on more expressive encodings, icluding the encoding of colouring semantics and intentinal automata to support context dependency.

Furthermore, I present our ideas about semantics for Reo expressed in mCRl2 that distinguishes handshaking mechanism from data flow and allows us to specify behavior of Reo circuits in presence of data transmission delays.

Eclipse Coordination Tools suite provides a user-friendly environment for designing Reo connectors. Our plug-in for automatic conversion from Reo to mCRL2 enables full-featured data-aware verification of service/component-based systems modeled in this environment.