Visualization of Reo specifications

Internal BCs project Formal Methods
Contact person Dr. Farhad Arbab, farhad.arbab@…

Reo [1] is a channel-based exogenous coordination language wherein complex connectors are compositionally constructed from basic channels. These connectors are used to couple software components and in this way create composite value-added software systems. Reo has a visual notation and a semantic model given by Constraint Automata (CA). Eclipse Coordination Tools (ECTs) is a tool suite consisting of Eclipse plug-ins for designing, animating and verifying connectors, as well as runtime engines for generating and executing coordination code. The construction of so-called glue-code by means of Reo connectors can be complex and error-prone, therefore, we use model checking tools to verify whether connectors meet their specifications. One of this tools is the Vereofy model checker [2] developed at the University of Dresden and integrated in the ECT environment. It uses two input languages, namely, Reo Scripting Language (RSL), and a guarded command language called Constraint Automata Reactive Module Language (CARML) which are textual versions of Reo and CA, respectively. The goal of this BCs project is to develop a tool for generating Reo connectors from RSL scripts, and CA from CARML scripts.

The BCs project fits with the current research of the SEN3 group at CWI in Amsterdam. A preliminary list of activities within the project is as follows:

  • getting acquainted with the Reo, RSL and CARML
  • develop an Eclipse plug-in that converts RSL/CARML scripts to Reo/CA models used by Reo editor and CA editor in the ECT environment.

References

  1. Farhad Arbab, Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), p329–366, 2004
  2. http://www.vereofy.de/