Simple tool for transforming 5G UML models to UPPAAL models.
You need Python (it has been tested with 3.7.6) as well as pip (python package installation tool). Moreover, it is also required to have UPPAAL [1] available on your computer.
Retrieve the source code by downloading (and extracting) ZIP-archive or using git:
git clone https://github.com/ptrbman/GGGGG.git
Afterwards, it is recommended to create a virtual environment:
cd GGGGG
python -m venv pyenv
source pyenv/bin/activate
Now install the required packages using pip:
pip install -r requirements.txt
Start the program by running the following in the root directory of the application:
python -m ggggg
Retrieve the source code by downloading (and extracting) ZIP-archive or using git:
git clone https://github.com/ptrbman/GGGGG.git
Afterwards, it is recommended to create a virtual environment:
cd GGGGGG
py -m venv pyenv
pyenv\Scripts\activate
Now install the required packages using pip:
pip install -r requirements.txt
Start the program by running the following in the root directory of the application:
python -m ggggg
In the settings tab you must select the location of the verifyta
and uppaal
binaries of the UPPAAL tool.
The application supports loading instances defined as a soil-script generated by the USE-tool [2].
In the details tab, details of the system are presented. It is also possible to search for a mapping which meets all deadlines. Note that UPPAAL is run in the background and the program does not resume until the search is finished. If the search takes a long time the program will freeze. The search is also highly sensitive to the values of Executors
and Message Queue Length
which are set in the settings tab.
In the verification tab it is possible to generate a UPPAAL model and check certain queries. The UPPAAL model generated will use the parameters Executors
and Message Queue Length
. Note that when a button is pressed, UPPAAL is run in the background and the program does not resume until query is finished. If the query takes a long time the program will freeze.
In this tab it is possible to perform K-fault tolerance check (currently k is always set to one and only hosts are removed). Note that when check is pressed, UPPAAL is run in the background and the program does not resume until query is finished. If the query takes a long time the program will freeze. It is also possible to select one of the found mappings and press "Study" to open that scenario in UPPAAL.
Here it is possible to set the location of the UPPAAL binaries as well as the parameters Executors
and Message Queue Length
.
The UML framework used is described in [3] and [4].
[2] https://sourceforge.net/projects/useocl/
[3] UML-based Modeling and Analysis of 5G Service Orchestration (Nov 2020) Ashalatha Kunnappilly, Peter Backeman, Cristina Seceleanu THE 27TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2020)
[4] From UML Modeling to UPPAAL Model checking of 5G Dynamic Service Orchestration (May 2021) Ashalatha Kunnappilly, Peter Backeman, Cristina Seceleanu 7th international Conference on the Engineering of Computer Based Systems (ECBS 2021)