Artifacts for SLE 2026

Description

Paper:

• Akram Idani, German Vega. Engineering Verified Model Transformations through a Proof-Based Language Workbench. ACM SIGPLAN International Conference on Software Language Engineering (SLE’2026). Accepted for publication.

Download archive:

• https://doi.org/10.5281/zenodo.19824411

The artifact archive contains an integrated Eclipse platform pre-configured for using BCerT and reproducing the experiments presented in the associated paper.

Claims Reproduced

This artifact reproduces the following claims from the paper:

• C0. Availability and executability of the BCerT tool.

• C1. Rule-based (ATL-like) model transformation execution.

• C2. Classical B transformation execution and generation of target models.

• C3. Event-B transformation execution using the event-based specification.

Contents of the Archive

The artifact archive contains:

• launch_bcert.sh
  macOS launcher script that removes quarantine attributes from the packaged Eclipse application and launches BCerT.

• bcert.app
  Pre-installed Eclipse Modeling environment (macOS, Apple Silicon ARM) including all required plugins. This is the recommended entry point for evaluators. If you prefer to use your own Eclipse platform, please refer to the BCerT Installation Guide.

• paper.pdf
  Accepted SLE paper associated with this artifact.

• README.md
  Artifact description and reproduction instructions.

• screenshots/
  Screenshots illustrating each execution step.

• bcert_dev/
  Development workspace containing:
  • source and target metamodels;
  • transformation metamodel;
  • formal B and Event-B specifications.
• bcert_run/
  Runtime workspace containing:
  • example input models;
  • generated transformation instances;
  • execution artifacts for reproducing experiments.

Step 1: Getting Started

Estimated setup time: few seconds.

Unzip BCerT-Artifact.zip. This creates the folder BCerT-Artifact.

Open a terminal in this folder and run:

./launch_bcert.sh

This removes the macOS quarantine attribute (if present) and launches the packaged Eclipse environment.

When Eclipse starts, choose a workspace location of your choice.

Step 2: Import Projects

To import the provided projects:

1. Open File → Import
2. Select General → Existing Projects into Workspace
3. Click Next

The import wizard is illustrated below.

1. Select the folder bcert_dev as the root directory.

2. Import all detected projects and click Finish.

The project selection step is illustrated below.

This imports three EMF projects:

• families, containing the source metamodel;
• persons, containing the target metamodel;
• transformation, containing the formal specification of the transformation.

In transformation/model/, the artifact includes the formal models corresponding to the three transformation strategies discussed in the paper:

• tr_ATL_Like.mch: a rule-based transformation specification inspired by the ATL approach;
• tr_Families2Person_BOp.mch: a Classical B specification expressing the transformation as operations constrained by invariants;
• tr_Families2Person_BEvent.sys: an Event-B specification modeling the transformation through events.

Step 3: Executing the Eclipse runtime

To launch BCerT, right-click on project transformation and select:

Run As → Eclipse Application

This launches a new Eclipse instance containing the BCerT runtime environment.

In the new Eclipse instance, import project FamilyModels from the artifact archive (folder bcert_run), using the same import procedure described previously.

This project contains two example source models:

• fam1.families
• fam2.families

These models are used as inputs for the Families-to-Persons transformation.

Step 4: Initializing the Transformation

To create a transformation instance, select:

File → New → Other → BCerT → Generate Transformation Instance

Click Next.

In the registered packages list, select: transformation (nsURI: http://transformation)

Click Next.

Set the output file extension to: persons

Then add the two source models to the selection, as shown below:

• fam1.families
• fam2.families

Click Finish.

Generated Artifacts: The transformation instance is generated within project transformation. For each input model (fam1.families and fam2.families), the following artifacts are created:

• a .persons model (e.g., fam1.persons, fam2.persons), corresponding to an initially empty target model. You may open these files and verify that they contain only the root element;

• a .transformation model (e.g., fam1.transformation, fam2.transformation), representing an instantiated transformation linking the source and target models.

At this stage, no transformation has been executed yet; only the transformation instances and their associated empty target models have been created.

The resulting structure is illustrated below.

Step 5: Running the Transformation

To execute a transformation, right-click on project transformation and select:

Run transformation

This opens a dialog asking you to select the B specification to be executed on the input models.

Select one of the three transformation specifications introduced above:

• tr_ATL_Like.mch
• tr_Families2Person_BOp.mch
• tr_Families2Person_BEvent.sys

Enable Parallel execution.

Click Finish.

This launches the execution of the generated transformation instances.

After execution, the generated target models fam1.persons and fam2.persons are populated with the transformed persons corresponding to the source family models.

Open both generated .persons files to verify that the transformation completed successfully.

The expected result is illustrated below.

Expected Successful Outcome

The artifact execution is considered successful if:

• fam1.persons contains transformed members of the Addams family;

• fam2.persons contains transformed members of the Simpson family;

• the Transformation Runner reports RUN FINISHED;

Citation

If you use this artifact, please cite: Akram Idani and German Vega. Engineering Verified Model Transformations through a Proof-Based Language Workbench. SLE 2026.