Solutions

The accepted solutions to the 2009 case studies can be found below. A ranking of the solutions can be found on the Awards page.

Synthesis

  1. Steffen Mazanek and Mark Minas. Transforming BPMN to BPEL Using Parsing and Attribute Evaluation with respect to a Hypergraph Grammar. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: The abstract syntax of structured Business Process Models (BPMs) can be described by a context-free hypergraph grammar in a straightforward way. Given a BPM, a hypergraph parser can be used to construct its derivation tree. Finally, the corresponding BPEL code can be generated using attribute evaluation. A diagram editor for structured BPMs has been realized using the DiaGen framework. On request, this editor outputs the BPEL code corresponding to the user's diagram.
  2. Steffen Mazanek and Mark Minas. Constructing a Bidirectional Transformation between BPMN and BPEL with Functional-logic Graph Parser Combinators. Paper (PDF) Try out the online demo in Online demo in SHARE...
    Abstract: The abstract syntax of structured Business Process Models (BPMs) can be described by a context-free hypergraph grammar in a straightforward way. Functional-logic graph parser combinators can be used to construct powerful parsers for such context-free hypergraph grammars. These parsers can be enriched with semantic computations, e.g. to synthesize BPEL from BPMN. Moreover, they are bidirectional by default thanks to their logic nature. Finally, functional-logic parsers stand out by their direct support for completion and language generation.
  3. Ruben Jubeh. BPMN to BPEL transformation with Fujaba - a Case Study. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: We have modeled a BPMN to BPEL synthesis transformation for the GraBaTs 2009 Tool Contest with the Fujaba Tool Suite. The basic problem of transformation is to create a hierachical a block structure out of a given flow graph. We use the same approach as already successfully implemented in the Fujaba code generator CodeGen2, which transforms amongst others SDM diagrams with arbitrary control flow into java code, which is as well formed as block structure.
  4. Maarten de Mol and Maria Zimakova. A GROOVE Solution for the GraBaTs'09 BPMN to BPEL Model Case Study. Paper (PDF), Attachment. Try out the online demo in Online demo in SHARE...
    Abstract: In this paper we present a solution of a model transformation between two standard languages for business process modeling BPMN and BPEL, using the GROOVE tool set. GROOVE is a tool for graph transformations that uses directed, edge labelled simple graphs and the SPO approach [7]. Given a graph grammar (G, P), composed of a start graph G and a set of production rules P, the tool allows to compute a labelled transition system (LTS) corresponding to all possible derivations in this grammar. The tool is freely available for download. The latest version and documentation can be found on the website http://sourceforge.net/projects/groove. The graph grammar presented here as well as detailed description of the sample realization to the case study is available in the attachment.
  5. Mark Asztalos, Tamas Meszaros and Laszlo Lengyel . Generating Executable BPEL Code from BPMN Models. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: Model transformations facilitate to process source models and generate other artifacts, output models and source code, based on algorithms and well-defined rules embedded into model transformations. Current paper presents two model transformations developed in Visual Modeling and Transformation System (VMTS) that facilitate the transformation between two languages for business process modeling: BPMN and BPEL. We also discuss how our model transformations achieve the case study related evaluation criteria: completeness, correctness, readability and reversibility.
  6. Guillaume Doux, Frédéric Jouault and Jean Bézivin. Transforming BPMN process models to BPEL process definitions with ATL. Paper (PDF), Attachment. Try out the online demo in Online demo in SHARE...
    Abstract: This paper presents a solution to the GraBaTs 2009 Case Study: BPMN to BPEL Model Transformation. This solution implements a bridge between two business process modeling languages, BPMN and BPEL. The proposed solution has been implemented using ATL.
  7. Gabor Bergmann and Akos Horvath. BPMN to BPEL case study solution in VIATRA2. Paper (PDF) (Online demo in SHARE demo will be available soon...)
    Abstract: This paper presents a solution to the BPMN to BPEL case study using the VIATRA2 framework
  8. Luciano Garcia Banuelos. Translating BPMN models to BPEL code. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: This paper describes a method for translating BPMN models to BPEL code. The method is based on the SQPR-tree decomposition and has been implemented as an Eclipse plugin. As this, the solution is implemented in Java language, and reuses several open-source packages: the STP BPMN Modeler, the OGDF graph manipulation framework. In the following section we describe the theoretical and pragmatical foundations of the tool.
  9. Olaf Muliawan, Bart Meyers and Dirk Janssens. BPMN2BPEL using MoTMoT. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: The case of transforming BPMN to BPEL (and back) presents some interesting challenges. Due to the lack of a meta-model for both formalisms, we have implemented our own using MDR. Despite the limited timeframe we were able to implement structured and quasi-structured process models quite rapidly. The structure of the patterns to be converted is very suitable for graph transformation techniques, in our case MoTMoT, based on Story Driven Modeling (SDM). Furthermore, on the one hand, the emphasis on speci?c transformation guidelines provides a basis for graph transformations with control ?ows. On the other hand, the different rules presented by the folding algorithm (transform sequence pattern, transform while pattern, ...) are best scheduled non-deterministically. Knowing this, modeling such a transformation elegantly turns out to be quite complex: new language features are useful to successfully model this in SDM. We explain how we use higher order transformations (HOTs) to translate these new language features into original SDM constructs in a platform independent manner.
  10. Claudia Ermel and Enrico Biermann. Transforming BPMN to BPEL with EMF Tiger. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: This paper describes a model transformation from the Business Process Modeling Notation (BPMN) to the Business Process Execution Language for Web Services (BPEL4WS, or BPEL for short). We give the meta-models for both source and target language as EMF models and de ne EMF model transformation rules using our recently developed tool EMF Tiger, an Eclipse plug-in supporting modeling and execution for EMF model transformations, based on structured data models and graph transformation concepts.

Reverse Engineering

  1. Sebastian Buchwald, Edgar Jakumeit and Moritz Kroll. A GrGen.NET solution of the Program Comprehension case for the GraBaTs 2009 Contest. Paper (PDF), Attachment. Try out the online demo in Online demo in SHARE...
    Abstract: A GrGen.NET solution of the Program Comprehension case for the GraBaTs 2009 Contest.
  2. Eduardo Zambon. Program Comprehension in GROOVE. Paper (PDF), Attachment. Try out the online demo in Online demo in SHARE...
    Abstract: This paper presents a solution to the program comprehension case study using the GROOVE tool.
  3. Frédéric Jouault and Jean-Sébastien Sottet. An AmmA/ATL Solution for the GraBaTs 2009 Reverse Engineering Case Study. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: This paper presents a solution to the reverse engineering case study of GraBaTs 2009 implemented using the AtlanMod Transformation Language (ATL), and the AtlanMod Model Management Architecture (AmmA). Two scalability approaches are presented: a classical one, as well as an optimization for multiple queries on the same model. The task showing the genericity of the transformation tool is also solved.
  4. Laszlo Angyal, Tamas Vajk and Gergely Mezei. VMTS Solution of Case Study: Reverse Engineering. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: Model-driven software development makes models and model transformations first-class citizens in software development. Program code and corresponding models evolve parallelly, thus round-trip engineering is highly required. Program code to model transformation plays a key role in program comprehension and examination as examining models is simpler than processing program code. In this paper, we introduce our solution to the reverse engineering case at GraBaTs'09 tool contest, in which filtering and transformation tasks have been proposed. The given solution utilizes model transformation described by graph transformation rules and a control flow language.

Verification

  1. Amir Ghamarian and Eduardo Zambon. Verifying the Leader Election Algorithm in GROOVE. Paper (PDF), Attachment. Try out the online demo in Online demo in SHARE...
    Abstract: This paper presents a solution to the verification case study using the GROOVE tool.
  2. Barbara Koenig and Vitaly Kozyura. Case Study: Verification of a Leader Election Protocol using Augur. Paper (PDF), Attachment. Try out the online demo in Online demo in SHARE...
    Abstract: We consider a case study of a leader election protocol and verify it using the tool Augur, which is based on unfolding techniques for graph transformation systems. We first investigate a finite-state variant of the leader election protocol and show how to verify it using McMillan-style unfoldings, avoiding an exponential explosion of the state space. Then, in a next step, we consider a parametric version based on attributed graph transformation.This variant is verified via approximated unfoldings in combination with counterexample-guided abstraction refinement.
  3. Albert Zuendorf. Model Checking the Leader Election Protocol with Fujaba. Paper (PDF). Try out the online demo in Online demo in SHARE...
    Abstract: We have developed a new library for Fujaba that provides explicit concepts for hierarchical graphs. These graphs come with a generic deep clone operation, a sophisticated hash function, and an isomorphism check for pairs of graphs. Given a set of rewrite operations, above graph functionalities enable us to compute reachability graphs, i.e. from an start graph we compute the set of all graphs that might be created by repeated application of the graph rules. In this case study we use these new features to do model checking for the leader election protocol.
  4. Gergely Mezei, Laszlo Siroki, Istvan Madari and Tamas Vajk. VMTS Solution of Case Study: Leader Election. Paper (PDF) . Try out the online demo in Online demo in SHARE...
    Abstract: Model-driven software development makes models and model transformations first-class citizens in software development. As programming is mostly replaced by modeling, verification of model transformation plays an important role in the process. We introduce our approach for validating a model transformation described by graph transformation rules and a control flow language. We present a method that translates the problem into the Prolog logical programming language, and creates a proof of correctness using the Prolog deduction engine.