This is the official python project for the bachelor thesis of Christoph Ueker.
| Title | Learning UPPAAL Timed Automata from Network Protocol Traces |
|---|---|
| Student | Christoph Ueker |
| Working period | 15.11.2021 - 15.02.2022 |
| University | Hamburg University of Technology (TUHH) |
| Insitute | Institute for Software Systems |
| Supervised by | Prof. Dr. Sibylle Schupp, Antje Rogalla |
| What was used | How it was used |
|---|---|
| Python | version 3.8.2 |
| PyCharm | version 2021.2.2 (Community Edition) |
| Windows | Windows 10 Pro version 21H1 |
| Packages | See requirements.txt |
The folder UPPAAL-Stratego contains the UPPAAL Stratego version 4.1.20-7 downloaded from uppaal.org. It contains uppaal.jar, which will run the created UPPAAL Model automatically. It also contains an executable called verifyta, which is used in order to run a simulate query.
The folder uppaalpy contains the module uppaalpy, which is a UPPAAL wrapper for python by Deniz Koluaçık. The used version 0.0.4 was committed on June 8th, 2021 downloaded from his github repository. WARNING: The module has been adjusted in order to work properly and to make things easier (Look for comments stating "adjusted" in nta.py).
The folder original_logs contains the logs given as examples in the original paper "Learning Timed Automata from Interaction Traces" by Vain et al.
The folder xml-files contains all Uppaal Timed Automata given as .xml files used throughout the project.
- Running main.py will run simulator.py first, asking the user for the interval abstraction parameter value (R), the number of environment nodes to be modelled and the desired number of simulations used in order to generate traces using the simulator.xml.
- simulator.py produces simulator_output.xml and query.q in order to use them in a verifyta command. The command writes the resulting simulation output to simulations.txt. Both files can be found in UPPAAL-Stratego/bin-Windows/.
- The conerter.py translates the simulation output to useful traces by applying a mapping.
- The produced traces will then be used by the algorithm implemented in main.py.
- main.py uses the library uppaalpy in order to create an UPPAAL system and later write it to output.xml.
- UPPAAL Stratego will be run in order to view the result.
- Helper functions have been outsourced to hepler.py
- Functions have been commented using docstrings, working nicely in PyCharm
- trace_converter_manual.py is an old backup module not part of the working code anymore