TRANSFORMASI PROMELA KE CHANNEL SYSTEM

Sheila Nurul Huda, Dr.-ing Mhd Reza Pulungan,

2012 | Tesis | S2 Ilmu Komputer

PROMELA adalah bahasa tingkat tinggi untuk mendeskripsikan model suatu sistem, sehingga dapat diverifikasi secara formal menggunakan tool model checker SPIN. Model sistem harus diimplementasikan dalam bahasa pemrograman tertentu, selama ini dengan implementasi manual yang memungkinkan terjadi kesalahan. Transformasi bahasa pemodelan menjadi bahasa implementasi adalah hal besar. Diawali dengan mengubah bahasa pemodelan dan bahasa implementasi menjadi struktur universal, yaitu Labeled Transition System (LTS) dan melakukan bisimulation. PRO- MELA tidak dapat diubah menjadi LTS begitu saja, sehingga perlu dilakukan dengan mengubah PROMELA menjadi Channel System. Penelitian ini membahas transformasi PROMELA ke Channel System. Channel System adalah sebuah cara untuk menggambarkan protokol komunikasi yang terjadi dalam sebuah sistem. Channel System disusun oleh Program Graph yang merupakan representasi proses-proses. Bagian utama Program Graph adalah perpindahan state/location yang terdiri dari lokasi awal (lo), guard yang menentukan apakah transisi ini dapat terjadi atau tidak, action yang akan dijalankan ketika terjadi perpindahan location, dan lokasi akhir (li). Struktur PROMELA berupa assignment, aksi komunikasi, if-fi, do-od, dan atomic step didefinisikan perpindahan location yang terjadi. File PROMELA dilexing untuk diketahui kata-katanya, kemudian di-parsing untuk diketahui strukturnya. Hasil parsing akan disimpan dalam struktur data internal yang berguna untuk men-generasi Channel System. Channel System yang dihasilkan diuji dengan pengujian beberapa struktur sederhana dan menunjukkan hasil yang sesuai. Pengujian dengan menggunakan sebuah contoh kasus yang cukup besar juga dilakukan dan menunjukkan hasil yang sesuai. Transformasi PROMELA ke Channel System telah berhasil dilakukan untuk struktur assignment, aksi komunikasi, do-od, if-fi, dan atomic step.

PROMELA is a high level language to describe a model of a system. System that has been modelled in PROMELA can be verified formally using SPIN model checker. The modelled system has to be implemented using one of the programming language. Up until now, the implementation is done manually which has possibility in mistakes. Transformation from modelling language to implementation language is a huge work, starting from translating the modelling and implementation language to a universal structure, named Labeled Transition System (LTS) and checking the bisimulation between them. PROMELA can not be translated to LTS as is, so that it is done by transforming PROMELA to Channel System. This paper deals with the transformation of PROMELA to Channel System. Channel System is a way to describe a communication protocol inside a system. Channel System consists of Program Graphs which represent a processes. The main element of Program Graph is a state/location transition which consists of beginning location (lo), guard which determines whether the transition is enabled or not, action that happened during the transition, and end location (li). PROMELA structures, such as assignment, communication action, if-fi, dood, and atomic step have to be defined in a transition locations. PROMELA file is lexed to get every word, the words then is parsed to get the structure. The parsing results are saved in internal data structures that will be used in generating Channel System. The Generated Channel System is validated by some basic structure and has shown an appropriate result. The validation is also done using quite complex test case and has shown appropriate result. Transformation of PROMELA to Channel System has successfully done for assignment, communication action, do-od, if-fi, and atomic step structures.

Kata Kunci : PROMELA, Channel System (CS), Program Graph (PG), transisi, transformasi.