METODE UNTUK MENGHASILKAN COUNTEREXAMPLE BERUKURAN MINIMAL PADA SPIN; A METHOD TO GENERATE MINIMAL COUNTEREXAMPLE FOR SPIN

Tuntari, Beti, Reza M. I.Pulungan

2015 | Skripsi | FMIPA UGM

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 : system verification; model checking; SPIN; counterexample; acceptance cycle; depth-first search; breadth-first search