In this second talk about Reo, I will briefly introduce several other semantic models that capture context-dependency in Reo connectors, namely, Intentional Automata and Reo Automata. Then I will introduce Action Constraint Automata which generalize Constraint Automata by allowing more observations on Reo ports. This model is used for describing behavior of Reo connectors with communication delays in channels. It also can capture context dependency.

The talk proceeds with the discussion of tools for validation and verification of Reo connectors. I will present the mapping of the aforementioned semantic models for Reo to process algebra mCRL2. This mapping allows us to apply tools from mCRL2 and CADP toolsets to simulate and model check Reo connectors extended with data expressions.

After that I will consider an extension of Reo with time-dependent channels, introduce Timed Constraint Automata and show how timed Reo connectors can be compositionally translated to the networks of timed automata, a specification format for the Uppaal model checker.

Finally, I will illustrate the application of Reo extended with data and time to service-based process modeling using two realistic examples.