Model checking of Reo connectors

Internal MSc project Formal Methods
Contact person Dr. Erik de Vink, HG 7.32 evink@…

The coordination language Reo is being developed at CWI in Amsterdam [1,2]. With Reo separate software components can be coupled, via a circuit-like Reo connector, for the computation of a joint task, for which the components rely on each other. In general, the construction of so-called glue-code is complex and error-prone. A major advantage of Reo is its being ‘exogenous’; components need not to be aware of the precise state or configuration of each other, they simply talk to the Reo connector. This paradigm shifts the issue of correctness to Reo. Methods and techniques need to be in place to verify whether a Reo connector meets its specification. In this MSc project we investigate the possibility of translating Reo in the mCRL2 modeling language for subsequent analysis using the mCRL2 toolset, developed in Eindhoven [3].

The MSc project fits with the current research of the Formal Methods group of TU/e, in cooperation with CWI in Amsterdam. The MSc thesis is aimed to form the basis of aresearch paper for an international workshop or conference. A preliminary list of activities within the project comprises

  • getting acquainted with the Reo and, if necessary, with mCRL2
  • working out the details of expressing Reo connects in mCRL2
  • application and fine-tuning of the technique for a number of smaller examples
  • a larger case study, e.g. in the field of service-oriented computing, or a comparison to an alternative approach based on so-called constraint automata [4].

This MSc project is meant for a student with an interest in formal methods and a which to pursue his/her career in academic research. The project is embedded in the research activities of the Formal Methods group at TU/e. Attending the ACG-seminar at CWI in Amsterdam, where regularly new developments in Reo are presented, is strongly advised. Knowledge of mCRL2, as taught in Eindhoven, is an advantage, but not necessary.

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://homepages.cwi.nl/~proenca/webreo/
  3. http://www.mcrl2.org
  4. Tobias Blechman and Christel Baier, Checking Equivalence for Reo Networks, Proceedings of FACS 2007, ENTCS 215, p209–226, 2008