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/