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

Discovery of process fragments and process reconfiguration

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

A business process is a collection of interrelated tasks (services) combined together to accomplish a particular goal. We can distinguish functional services performing self-contained business operations, and coordination services, realizing so called 'glue code'. Traditional graphical notations for business process modeling such as BPMN and UML Activity Diagrams (ADs) represent business processes in a form of abstract tasks (activities) with a control flow over them. Formal notations such as Petri nets, process algebras, transition systems or logic-based languages are useful for unambiguous business process specification and analysis. Recently we applied the channel-based exogenous coordination language Reo [1] to model business process workflows [2]. Operational semantics for Reo is given by Constraint Automata (CA), a variant of a labeled transition system, which enable process analysis using model checking tools, comparison of their behavior and automated adaptation and/or redesign. In this context, the following tasks appear:

  • Given two Reo/CA process fragments, compare their behavior.
  • Given a Reo/CA process fragment and a set of Reo/CA process models, find processes containing this fragment.
  • Given two Reo/CA process fragments, source and target, and a Reo/CA process model, find all entrances of the source fragment in the process and substitute it with the target fragment.

Process fragment matching can be realized by checking equivalence of Reo connectors [3]. However, similar activities can have different names in different implementations of the process. Therefore, behavioral equivalence checking should be combined with syntactic and/or semantic process matching.

The preliminary list of activities for this MSc project include the following:

  • get acquainted with busines process modeling, Reo, notion of bisimulation equivalence for CA and ontology-based semantic matching techniques,
  • implement a tool to resolve the aforementioned tasks,
  • prepare a research paper for an international workshop or conference.

This MSc project is part of research on compliance-aware business process modeling and verification conducted by SEN3 group at CWI, Amsterdam, within the EU FP7 COMPAS project


  1. F. Arbab, Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), p329-366, 2004.
  2. F. Arbab, N. Kokash, and M. Sun. Towards using Reo for compliance-aware business process modelling. In Proceedings of the ISoLA 2008, vol. 17 of LNCS. Springer, 2008.
  3. T. Blechman and C. Baier, Checking Equivalence for Reo Networks, Proceedings of the FACS 2007, ENTCS 215, p209-226, 2008.