The Gamma Statechart Composition Framework

Version 2.11.0 - For the latest version, check out the dev branch.

The Gamma Statechart Composition Framework is a toolset to model, verify and generate code for component-based reactive systems. The framework builds on Yakindu, an open source statechart modeling tool and provides an additional modeling layer to instatiate a communicating network of statecharts. Compositionality is hierarchical, which facilitates the creation of reusable component libraries. Individual statecharts, as well as composite statechart networks can be validated and verified by an automated translation to

• UPPAAL, a model checker for timed automata,
• Theta, a generic, modular and configurable model checking framework,
• Spin, a tool for the formal verification of multi-threaded software applications, or
• nuXmv, a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems. Once a complete model is built, designers can use the code generation functionality of the framework, which can generate Java code for the whole system.

Check out http://gamma.inf.mit.bme.hu for more resources about Gamma. A good starting point is our tool paper, slides and demo video presented at ICSE 2018 as well as our journal paper.

To cite Gamma, please cite the following paper. You can find additional publications about Gamma here.

@inproceedings{molnar2018gamma,
    author = {Vince Moln{\'{a}}r and
              Bence Graics and
              Andr{\'{a}}s V{\"{o}}r{\"{o}}s and
              Istv{\'{a}}n Majzik and
              D{\'{a}}niel Varr{\'{o}}},
    title = {The {Gamma Statechart Composition Framework}: design, verification and code generation for component-based reactive systems},
    booktitle = {Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings},
    pages = {113--116},
    year = {2018},
    publisher = {ACM},
    doi = {10.1145/3183440.3183489}
}

Using Gamma

Dependencies

Recommended Eclipse version and bundle:

• Eclipse IDE 2023-09, Eclipse IDE for Java and DSL Developers bundle. Note that Yakindu (see below) will not work with the 2023-12 or newer Eclipse releases due to compatibility reasons.

3rd-party Eclipse components (should be installed separately):

• Xtext 2.32.0 (https://www.eclipse.org/Xtext/, included in Eclipse bundle),
• VIATRA 2.8.0 (https://www.eclipse.org/viatra/),
• Yakindu Statechart Tools 3.5.13 (https://www.itemis.com/en/yakindu/state-machine/),
• PlantUML 1.1.30 (https://plantuml.com/).

3rd-party tools used by Gamma (should be installed separately):

• UPPAAL (Uppsala and Aalborg Universities, http://www.uppaal.org/),
• Spin (Available under the standard BSD 3-Clause open source license, https://spinroot.com/),
• nuXmv (Fondazione Bruno Kessler, https://nuxmv.fbk.eu/).

Installation

• Install an Eclipse instance (e.g., Eclipse IDE for Java and DSL Developers) with EMF, Xtext and Java 17.
• Install the required 3rd-party Eclipse components. Detailed instructions can be found in the plugins/README.md file.
  • Alternatively you can use the provided Eclipse Oomph Installer to install the 3rd-party Eclipse components found here.
• Exit Eclipse and extract the Gamma zip file containing the dropins/plugins folder (with the Gamma JAR files) into the root folder of Eclipse. This will create the plugins directory in the dropins folder of your root Eclipse folder, which should contain all JAR files of Gamma. (If not, make sure you copy all the JAR files contained in the Gamma zip file in the plugins directory of the dropins folder of the root folder of Eclipse.)
• When starting Eclipse for the first time, you might need to start it with the -clean flag.
• Check if the plugin installed successfully in Help > About Eclipse and by clicking Installation Details. On the Plug-ins tab, sort the entries by Plugin-in Id and look for entries starting with hu.bme.mit.gamma.
• For formal verification, download and extract UPPAAL. In order to let Gamma find the UPPAAL executables, add the bin-Win32 or bin-Linux folder to the path environment variable (depending on the operating system being used).
• If you want to use Theta, check out the installation steps here.
• If you want to use Spin, check out the installation steps here.
• If you want to use nuXmv, check out the installation steps here.
• If you want to use xSAP, check out the installation steps here.

Tutorials

The tutorials for the framework can be found in the following folder.

Contact

Contact us by sending an e-mail to gamma [at] mit.bme.hu.

Acknowledgement

Supporters of the Gamma project:

• MTA-BME Lendület Cyber-Physical Systems Research Group,
• Fault Tolerant Systems Research Group, Department of Measurement and Information Systems, Budapest University of Technology and Economics,
• Új Nemzeti Kiválóság Program (ÚNKP) 2017-2018,
• Új Nemzeti Kiválóság Program (ÚNKP) 2019-2020,
• Új Nemzeti Kiválóság Program (ÚNKP) 2020-2021,
• Új Nemzeti Kiválóság Program (ÚNKP) 2022-2023,
• Új Nemzeti Kiválóság Program (ÚNKP) 2023-2024,
• Emberi Erőforrás Fejlesztési Operatív Program (EFOP) (EFOP-3.6.2-16-2017-00013),
• NRDI Fund of Hungary (2019-2.1.1-EUREKA-2019-00001 EMBrACE project),
• EU ECSEL and NRDI Fund of Hungary (EU ECSEL 826452 and NRDI Fund 2019-2.1.3-NEMZ_ECSEL-2019-00003 Arrowhead Tools project), and
• Versenyképességi és kiválósági együttműködések program (VKE) (2018-1.3.1-VKE-2018-00040 projekt).

Special thanks to:

• András Vörös,
• Oszkár Semeráth,
• Kristóf Marussy,
• Ákos Hajdu,
• Dániel Varró,
• István Ráth,
• Zoltán Micskei,
• István Majzik,
• IncQuery Labs Ltd.