Metode untuk Menghasilkan Counterexample Berukuran Minimal pada SPIN

BETI TUNTARI, Mhd. Reza M.I Pulungan, M.Sc., Dr.-Ing

2015 | Skripsi | S1 ILMU KOMPUTER

Kesalahan yang terdapat pada suatu sistem, terutama sistem yang kritikal, dapat mengakibatkan sesuatu yang fatal. Oleh karena itu, kesalahan pada sebuah sistem harus diminimalisasi. Salah satu cara meminimalisasinya adalah dengan menggunakan model checking. Model checking digunakan untuk membuktikan bahwa suatu sistem telah memenuhi properti-properti yang ditentukan. Ketika sistem tidak memenuhi properti-properti tersebut, counterexample akan dihasilkan. Lalu counterexample itu lah yang akan dianalisis dan digunakan sebagai dasar untuk memperbaiki sistem tersebut. Ukuran counterexample akan mempengaruhi proses analisis dan perbaikan sistem. Counterexample yang berukuran panjang akan mempersulit proses analisis dan perbaikan sistem. Sementara counterexample yang pendek akan mempermudah proses tersebut. Dengan demikian, proses model checking harus menghasilkan counterexample yang berukuran pendek. SPIN adalah suatu perangkat lunak yang bisa digunakan untuk melakukan model checking. SPIN akan memverifikasi model sistem dan sebuah properti. Jika model sistem tidak memenuhi properti, counterexample akan dihasilkan. SPIN menggunakan algoritma pencarian depth-first search (DFS) untuk menghasilkan counterexample. Penelitian ini menggunakan metode lain yang berdasarkan penelitian Gastin dan Moro (2007) untuk menghasilkan counterexample berukuran minimal pada SPIN. Metode ini menggunakan algoritma breadth-first search (BFS) yang telah ada di kode program SPIN untuk menghasilkan counterexample berukuran minimal. Counterexample yang dimaksud adalah counterexample yang berbentuk acceptance cycle. Hasil pengujian menunjukkan bahwa SPIN yang telah dimodifikasi menghasilkan counterexample yang lebih pendek atau sama dengan SPIN yang tidak dimodifikasi.

Errors in systems, especially safety-critical systems, can cause something fatal. Therefore, errors in a system should be minimalized. There are some techniques to do that. One of them is called model checking. Model checking is used to prove that a system satisfies some certain properties. If the system doesn't satisfy the properties, counterexample will be produced. Then, the counterexample will be analyzed and used as the basis for correcting the system. Counterexample size will affect analysis process and process to correct the system. Large counterexamples will make those processes more complicated. On the other hand, small counterexamples will make them easier to do. So, model checking process should compute small counterexample. SPIN is a software that can be used to perform model checking. SPIN will verify a system model and a certain property. If the property is violated by the system model, SPIN will produce a counterexample. SPIN uses depth-first search algorithm to compute counterexamples. In this research, we use another method, based on Gastin and Moro's (2007) research, to generate minimal counterexample for SPIN. We use breadth-first search algorithm that has already existed in SPIN's source code to generate minimal counterexample. Counterexamples addressed in this research are acceptance cycle. The result of this research shows that the modified SPIN can generate equal or smaller counterexamples than the unmodified one.

Kata Kunci : verifikasi sistem, model checking, SPIN, counterexample, acceptance cycle, depth first search, breadth first search