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

DRS. SUPRAPTO, M. KOM, Drs. Retantyo Wardoyo, M.Sc., Ph.D; Prof. Dra. Belawati H. Widjaja, M.Sc., Ph.D; Dr.-Ing. MHD. Reza M.I. Pulungan, S.Si, M.Sc.

2015 | Disertasi | S3 Ilmu Komputer

Penerapan software sering menentukan atau mengendalikan perilaku-perilaku sistem, sehingga software mempunyai peran yang besar dalam jalannya sebuah sistem. Khususnya untuk sistem-sistem yang reaktif atau critical, kesalahan yang terjadi pada software akan mengakibatkan kerugian yang sangat besar, baik kerugian materi maupun non-materi. Oleh karena itu, software dalam sistem-sistem semacam ini harus direkayasa (engineered) dengan tingkat keseriusan yang tinggi untuk mengantisipasi perilaku yang tidak bisa diperkirakan sebelumnya dari sistem. Sudah banyak penelitian yang telah berhasil melakukan pemastian kebenaran (correctness) sistem melalui modelnya, yang dikenal dengan model checking. Keluaran model checking adalah model sistem yang sudah dicek kebenarannya oleh tool atau aplikasi yang disebut pengecek model (model checker). Model sistem bukan sistem yang sesungguhnya, sehingga untuk mendapatkan sistem yang sesungguhnya perlu implementasi dengan penulisan kode dalam bahasa pemrograman tertentu. Pada umumnya, penulisan kode program secara manual oleh penulis program (programmer) rentan terhadap kesalahan (error prone). Oleh karena itu, perlu ada sebuah mekanisme yang secara otomatis mampu menghasilkan (generate) program dari model, dan menjamin kebenaran model tetap dipertahankan dalam sistem yang dihasilkan. Dalam disertasi ini dikembangkan sebuah model translasi dengan pendekatan asosiasi konstruk (construct association - CA) antara bahasa pemodelan PROMELA sebagai bahasa sumber dengan bahasa pemrograman Java sebagai bahasa target. Selanjutnya, untuk menjamin kebenaran translasi, dikembangkan aturan pembandingan yang memperlihatkan ekuivalensi semantik antara setiap pasangan asosiasi konstruk. Akhirnya, dengan terbuktinya ekuivalensi semantik antara setiap pasangan asosiasi dibutikan ekuivalensi antara model PROMELA dengan hasil translasinya, program Java. Di samping itu, sebagai hasil implementasinya, dikembangkan sebuah tool yang mengotomatisasi translasi kode yang mempertahankan semantik.

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 systemmodel 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.