| Abstract [eng] |
In this research, we investigate a methodology that ensures the compliance of Elixir programs with TLA+ specifications, developed by software engineers. The main component for linking the Elixir code with TLA+ specifications are translation rules. These rules were defined and utilized during the implementation of a translation method, which is capable of converting sequential Elixir code into TLA+ specifications. The correctness of the generated specifications is evaluated through model checking and refinement techniques, while the correctness of the translation method is ascertained by converting the generated specifications back to Elixir code and by conducting unit tests of the source program. |
