TRANSFORMASI CHANNEL SYSTEM KE LABELLED TRANSITION SYSTEM

SITI MUTMAINAH, Dr. Ing. Mhd Reza M.I Pulungan, S.Si., M.Sc.,

2012 | Tesis | S2 Ilmu Komputer

Sistem paralel harus dibangun dengan kecermatan yang ekstra untuk mencapai tingkat dependabilitas yang tinggi agar menghasilkan software yang bebas kesalahan. Oleh karena itu diperlukan model sistem yang tepat dan formal. Model tersebut digunakan untuk proses verifikasi sotfware dalam model checking. Salah satu model yang sering dipakai dalam model checking adalah LTS (Labelled Transition System). LTS dapat dihasilkan melalui Program Graph (PG) yang merupakan bentuk representasi dari bahasa pemrograman. Namun karena yang dimodelkan adalah sistem paralel, maka diperlukan model komunikasi untuk menggambarkan interaktifitas antar PG sehingga digunakan Channel System (CS). Dari permasalahan di atas, diperlukan adanya proses transformasi dari CS ke LTS agar dari sebuah model sistem paralel dapat diketahui semantik operasionalnya dengan jelas. Untuk itu dibuat sebuah algoritma transformasi untuk menghasilkan LTS dari sebuah CS. Melalui konsep paralelisme, algoritma tersebut berjalan dengan mengekploitasi sebuah pendekatan yaitu SOS (Structured Operational Semantic). Algoritma transformasi diimplementasikan dengan membangun sebuah tool prototype yang dirancang dengan 3 komponen penting, yaitu input, proses dan output. Input adalah file teks yang merupakan model dari sistem paralel berupa CS. Kemudian model tersebut akan diproses dengan menggunakan algoritma transformasi sehingga menghasilkan output berupa file LTS. Secara fungsional, algoritma ini mampu menangani model sistem paralel yang ditulis dengan CS yang di dalamnya terdapat berbagai macam bentuk PG baik yang mengandung perulangan maupun percabangan. Selain itu algoritma ini mampu menangani proses paralel seperti interleaving, synchronous dan asynchronous. Sedangkan secara performance, dapat diukur elapsed time dan memory yang terpakai untuk menghasilkan sejumlah state. Hasil pengujian menunjukkan bahwa elapsed time dan memory cenderung meningkat seiring dengan pertumbuhan state, walaupun hal ini sangat bergantung pada model PG yang digunakan di dalam CS.

Parallel system must be developed with extra precision to achieve a high level of dependability to produce error-free software. Therefore we need appropriate and formal model of system. The model is necessary for verification software in model checking. A model often used in model checking is LTS (Labelled Transition System). LTS can be generated by Program Graph (PG) which is representation of programming language. However, modeling parallel system needs to describe the communication model of interactivity between a PG and another PG. So, the model can use Channel System (CS). To solve this case, it is necessary to transform CS to LTS. So, the aim of the research is developing transformation algoritm to generate LTS from a CS. Through the concept of parallelism, the algorithm is run by exploiting the so-called SOS (Structured Operational Semantic) approach. Transformation algorithm is implemented by developing a prototype tool designed with 3 essential components, input, process and output. Input is a text file that contains a model of a parallel system in form of CS. The model will be processed by using a transformation algoritm that generates LTS as output file. Functionally, the algoritm can handle model of parallel system written by CS that consists of various form of PG containing both looping and branching. Moreover, it has ability to satisfy parallel process such as interleaving, synchronous and asynchronous. In the performance testing, we can measure elapsed time and memory used to produce states. The results of the research show that elapsed time and memory tend to increase with the growth number of state, although it depends on the PG model used in the CS.

Kata Kunci : Labelled Transition System (LTS), Channel System (CS), Program Graph (PG), model, paralel.