🔩📜🧩🧪🪒
Table of Contents
Pipeline overview:
This repository contains the artifacts generated and used during the work on my Master’s thesis. It includes custom modules, automatically generated Erlang code, test results, translation code, and batch scripts.
A formal TLA⁺/PlusCal specification of the Erlang/OTP GenServer was developed and verified through model checking, and this specification was extended with a translation pipeline that automatically generates correct and usable Erlang GenServer code, which successfully passed the official OTP test suite and additional QuickCheck tests.
For the generated GenServer that was derived from the TLA⁺ specification compared to the original implementation, the following differences were observed:
| Subfolder | Explanation | Link |
|---|---|---|
custom-module/ |
Contains manually written Erlang modules that complement or extend the automatically generated GenServer code. | custom-module |
gen-server-out/ |
Contains the automatically generated Erlang files (GenServer implementation). These files are generated from PlusCal specifications and should not be manually modified. | gen-server-out |
gen-server-suite-results/ |
Contains the Common Test (CT) logs and results from executing the generated GenServer test suite. Mainly for validation and traceability. | gen-server-suite-results |
slurm-scripts/ |
Contains batch scripts for SLURM to execute TLC model checking in a cluster environment. These scripts handle automated runs of the verification process. | slurm-scripts |
translation/ |
Contains the Java implementation responsible for automatically extracting Erlang code from PlusCal specifications. This is the translation layer between formal specification and executable Erlang. | translation |