Extensible Coordination Tools
The Extensible Coordination Tools (ECT) are a set of plug-ins for the Eclipse platform. The tools currently support:
- Graphical editing of Reo connectors and (variations of) constraint automata.
- Animation of Reo connectors using on-the-fly generated Flash bytecode.
- Code generation from Reo connectors or constraint automata.
- Generation of propositional formulas with linear arithmetic from Timed Constraint Automata, for use in bounded model checking
- Dynamic reconfiguration of connectors using algebraic graph
- Model checking connectors using Vereofy and mCRL2.
- Simulation of stochastic Reo connectors for QoS analysis.
- Conversion of BPEL models, UML2 Activity Diagrams and Sequence Charts to Reo.
The animation tool gives an idea of how a particular channel works in specific context. The small example animation below was generated using the current version of the tools.
The plug-ins can be installed using the update manager of Eclipse. The following software is required to run the tools:
To install the coordination tools, add a new remote update site in the update manager using the below URL. For updating an exisiting installation, click on Check for updates in the Help menu of Eclipse.
To install the BPMN2Reo converter, Eclipse requires additional third-party plugins from the STP project. In order to install those plugins, please download and copy the following files into the "dropins" folder in the Eclipse root directory:
You may also need to add -clean to the "eclipse.ini" file (or run eclipse with the --clean flag). Afterwards, Eclipse should be able to install the BPMN2Reo converter.
Because of the dependencies to the out-dated packages, the BPMN2Reo converter is currently not part of the ECT releases.
A common problem on Linux machines seems to be that the animation is not working, e.g. that it asks you to install a Flash plug-in or it doesn't show anything. You can try the following to fix this problem. Find the file libflashplayer.so on your system. It is probably located under /usr/lib/mozilla/plugins. On 64-bit machines this file has a different name. On Fedora it is /usr/lib64/mozilla/plugins-wrapped/nswrapper_32_64.libflashplayer.so. Then, as a normal user do this:
cd ~/.mozilla/plugins ln -s <absolute-path-of-flash-library>
Then start Eclipse again and see if it works.
We have a user manual and a couple of live demos of ECT:
Distributed Reo Engine
The Distributed Reo Engine (Dreams) is a framework where different coordination primitives execute in a distributed environment, without a centralised coordinator.
Each Reo channels is coordination primitive. Coordination primitives are connected via nodes, which are special instances of these primitives.
- Coordination Primitive
- Has several (distributed) ports that can be connected to nodes;
- Messages flowing on ports obey a certain protocol to ensure correct (synchronous) behaviour of the whole connector.
- Stateless connector that propagates synchronous constraints;
- Glues different locations.
An engine represents a process executing in a single machine where different primitive objects (coordination primitives and nodes) can be deployed. The diagram below illustrates the execution of several coordination primitives and nodes executing in different engines, where each engine is represented by a different colour.
For more information follow one of the links below:
Vereofy Model Checker
Vereofy is a formal verification tool developed by the TU-Dresden in the context of the EU project CREDO and the DFG/NWO-project SYANCO. The model checker can be used as a stand-alone tool or via an Eclipse plug-in that integrates with the ECT. For more information on Vereofy see the project homepage: