State Space-Based Methods for Validating Model Transformations in Model Checkers (Dataset)

Artifact These directories contain all necessary files and our results for our evaluation, and additionally, to our motivation example for the paper titled "State Space-Based Methods for Validating Model Transformations in Model Checkers" by Zsófia Ádám and Zoltán Micskei. These files are available directly in the zenodo archive, but the provided Ubuntu VM also contains a copy of this directory. DOI of the paper: TBA About the Virtual Machine VM username and password: artifact The VM is a simple ubuntu 24.04.1 Desktop install with the following additional packages (and their dependencies) installed from apt:openssh-servergraphvizdotopenjdk-17-jre-headless It has 8GB of RAM, a 35GB disk and 12 CPU cores. It is a kvm VM, thus a qcow2 disk and the exported XML of the VM is provided. Change the <file> path to the qcow2 file before importing it. Data Folders These are available separately and on the virtual machine as well. Motivation Example This is the motivation example of HugoRT battery models from the beginning of the paper. Evaluation This is our main evaluation executed on the Gamma-Theta toolchain from the last section of the paper. Textual source (gcd extension) and PlantUML visualisations for each model are also provided, eliminating the need to run Gamma and the Eclipse IDE for just checking the model suite. Both the evaluation and the motivation example include their own readmes.