A SEMANTIC-PRESERVING CODE TRANSLATION FROM PROMELA MODEL TO JAVA PROGRAM USING CONSTRUCT ASSOCIATION

Suprapto, Retantyo Wardoyo

2016 | Tesis | FMIPA

Software implementation frequently determines or controls system’s behavior, so that, software has an important role in determining the success of system’s operation. The failure occurring on software especially for reactive or critical systems will imply a huge loss both material and immaterial. Therefore, software that implemented in these kinds of systems must be engineered with high level of accuracy in order to anticipate the unpredicted behavior of system beforehand. There have been many researches had succeeded in performing systems’s correctness checking via their models, it is known by model checking. The output of model checking is a system model that has been checked their correctness by either a tool or an application called by a model checker. A system model is not an actual system, therefore, in order to obtain the actual one the model still need to be implemented by manually writing program’s codes in certain programming language. In general, however, manually coding by a computer programmer tends to make some errors (error prone). It motivates to develop a mechanism that automatically generates a program from a model, and guarantee to preserve the correctness of the model in the generated program. In this research, a model of translation is developed with a construct association’s approach – the construct association (CA) from the source language PROMELA to the target language Java. Subsequently, in order to guarantee the correctness of translation model, it is developed the comparison rules showing semantics equivalence between every pair of constructs in association. Finally, having proven the semantic equivalence for every construct association, it will prove the equivalence semantic between PROMELA model and Java program. In addition, as another result, it is developed a semantic preserving tool or application to automatically generate a Java program from a checked model PROMELA.

Kata Kunci : PROMELA model , safety critical, correctness, model checker, error prone, semantics equivalence, Java program, automatic transition