Deprecated: this webpage is preserved for archival purposes. Please consider visiting the new Reo webpage.

Visualization of Reo model checking results

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. Vereofy supports linear and branching-time model checking. If some formula does not hold, the model checker provides a counterexample, which is essentially a part of the connector execution path, i.e., a set of transitions in the corresponding CA. The goal of this BCs project is to develop a tool for visualizing model checking counterexamples.

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, ECT and Vereofy
  • develop a tool that shows execution paths from counterexamples using animation engine 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/