Suprapto, M.Kom

Permasalahan utama yang muncul dalam model cheking terhadap sistem reaktif atau sistem konkuren adalah state-space explosion, yaitu banyaknya state dalam ruang state dari sistem-sistem kompleks yang besar bisa luar biasa besar, bahkan bisa tak-berhingga, sehingga tidak mungkin melakukan eksplorasi ruang state secara menyeluruh. Sehingga banyak penelitian yang bertujuan mengurangi (atau mereduksi) ukuran ruang state.
Dalam penelitian ini diusulkan sebuah pendekatan heuristik dengan algoritma genetika untuk menyeleksi (secara random) path-path transisi state yang perlu dicek. Path-path yang dimaksud, direpresentasikan sebagai string of states dan selanjutnya disebut kromosom. Dengan bantuan model checker, path-path tersebut dicek untuk mengetahui apakah ada state error yang bisa dicapai (reachable error states).

Latar Belakang :

Banyaknya states dalam sejumlah variabel dalam graph program, misal untuk N variabel dengan sebuah domain dengan k nilai-nilai yang mungkin; banyaknya state berkembang menjadi k^N. Pertumbuhan eksponensial ini juga dikenal sebagai permasalahan state-space explosion (Baier dan Katoen, 2008). Bahkan untuk graph program sederhana sekalipun yang hanya dengan sejumlah kecil variabel, batasan ini bisa agak berlebihan. Sebagai contoh, sebuah graph program dengan sepuluh lokasi, yang terdiri dari tiga variabel Boolean dan lima interger terbatas (dengan domain dalam {0, 1, …, 9}) mempunyai 10×2³x10⁵ = 8.000.000 states. Seandainya sebuah array bit tunggal dengan 50 bit ditambahkan ke graph program (contoh), batas ini bahkan berkembang menjadi 800.000×2⁵⁰. Secara jelas pengamatan ini memperlihatkan mengapa verifikasi terhadap sistem-sistem data–intensive (dengan banyak variabel atau domain-domain yang kompleks) sangat sulit. Sehingga meskipun dalam sebuah program hanya ada sejumlah kecil variabel, akan tetapi ruang state yang harus dianalisa bisa sangat besar.

Model checking merupakan salah satu teknis otomatis untuk memverifikasi sistem-sistem konkuren state-berhingga, yang secara khusus melibatkan pencarian menyeluruh terhadap ruang state dari sebuah sistem untuk menentukan apakah suatu property dari sistem dipenuhi atau tidak. Sudah banyak teknik-teknik eksplorasi ruang state (state space) digunakan secara sukses untuk mendeteksi kesalahan-kesalahan penting yang belum (tidak) kelihatan dalam rancangan dan implementasi dari beberapa sistem reaktif konkuren hardware maupun software. Tujuan praktis utama dari eksplorasi ruang state adalah untuk menemukan kesalahan-kesalahan (errors) yang sulit dideteksi.

Batasan praktis utama ketika melakukan model checking terhadap sistem-sistem reaktif konkuren adalah berurusan dengan apa yang disebut permasalahan state-space explosion, yaitu banyaknya state yang termuat dalam ruang state dari sistem-sistem kompleks yang besar bisa luar biasa besar dan bahkan tak-berhingga. Sudah banyak pendekatan-pendekatan yang diusulkan untuk menyelesaikan permasalahan state-space explosion, termasuk verifikasi  simbolik, metode-metode partial-order, metode-metode simetri, dan sebagainya. Meskipun pendekatan-pendekatan ini telah meningkatkan cakupan model checking ke ruang state-ruang state dengan jumlah state dalam order yang lebih besar, akan tetapi masih banyak ruang state masih terlalu besar untuk ditangani. Sehingga state-explosion masih menjadi permasalahan mendasar dalam model checking.

Ketika sebuah permasalahan secara komputasional sulit diselesaikan menggunakan sebuah algoritma yang  pasti dan lengkap, dalam ilmu komputer biasanya diselesaikan dengan menggunakan pendekatan heuristik untuk mendapatkan penyelesaian-penyelesaian pendekatan terhadap permasalahan, atau untuk mengarahkan ke penyelesaian secara lebih cepat. Meskipun ide pemanfaatan heuristik untuk model checking sulit untuk diterima, karena model checking bukan permasalahan optimasi. Di samping itu, dengan menggunakan pendekatan heuristik justru menghindari pengecekan secara menyeluruh terhadap jalur-jalur transisi yang ada (mungkin dalam ruang states. Akan tetapi, apabila dilihat dari tujuannya yaitu mencari jalur-jalur tertentu saja yang berpotensi memuat error state yang harus dicek oleh model checker, berarti letak optimasinya pada peminimalan banyaknya jalur-jalur transisi state yang harus dicek. Sehingga pemanfaatan heuristik dalam model checking bisa diterima.

Dalam penelitian ini diusulkan sebuah model yang menggunakan algoritma genetika untuk memanfaatkan heuristik dalam menentukan jalur-jalur transisi mana yang harus dilakukan pengecekan oleh (dengan bantuan) model checker. Jalur-jalur yang direkomen-dasikan oleh algoritma genetika selanjutnya akan dieksekusi oleh model checker untuk mengetahui apakah ada error state di dalamnya. Keberadaan error state dalam suatu jalur akan digunakan sebagai nilai fitness dari kromosom yang merepresentasikan jalur transisi tersebut.

Tujuan Penelitian

Seperti penelitian-penelitian yang lain khususnya untuk area state explosion problems, penelitian inipun bertujuan mengarahkan (atau merekomendasikan) model checker untuk melakukan pengecekan terhadap jalur-jalur transisi state yang mempunyai potensi untuk memuat error state. Adapun kontribusinya adalah sebuah usulan tentang cara lain bagaimana merepresentasikan jalur-jalur transisi state tersebut ke dalam bentuk kromosom dalam algoritma genetika. Di samping itu, dalam penelitian ini juga akan diusulkan cara lain komunikasi antara model checker dengan model algoritma genetika.

Urgensi Penelitian

Seperti yang sudah disebutkan di depan, bahwa salah satu permasalahan yang menghambat dalam model checking adalah peningkatan ukuran ruang sampel yang sangat cepat (secara eksponensial) seiring dengan meningkatnya kompleksitas sistem. Sehingga banyak penelitian yang sudah dilakukan dalam area ini bertujuan untuk mereduksi ukuran ruang state dengan tetap menjaga tercapainya tujuan utama dalam proses model checking.

Pada umumnya penelitian-penelitian dilakukan dengan berawal dari penelitian yang sudah ada (dilakukan sebelumnya) dengan tujuan (harapan) bisa memperbaiki hasil yang sudah dicapai sebelumnya menggunakan cara, teknik atau metode yang bisa berbeda. Seperti halnya penelitian ini yang dilakukan dengan berawal pada penelitian yang sudah dilakukan (sudah ada) (Godefroid, P., dan Khurshid, S., 2002). Selanjutnya, dalam penelitian ini diusulkan suatu cara lain dalam merepresentasikan penyelesaian suatu permasalahan yang akan diselesaikan, yaitu jalur-jalur transisi state yang harus dieksekusi (dicek) oleh model checker untuk menentukan ada tidaknya error states. Harapannya, dengan cara representasi ini akan lebih banyak mereduksi ukuran ruang state dibanding dengan hasil dari penelitian sebelumnya

Studi Pustaka :

DAFTAR PUSTAKA

Alur, R., Brayton, R. K., Henzinger, T. A., Qadeer, S., dan Rajamani, S. K., 1997, Partial-Order Reduction in Symbolic State Space Exploration, Proceedings of the 9th International Conference on Computer-aided Verification (CAV 97), Lecturer Notes in Computer Science 1254, Springer-Verlag, 1997, pp. 340-351.

Baier, C. dan Katoen, J. P., 2008, Principles of Model Checking, The MIT Press, Cambridge, Massachusetts, 2008.

Basagiannis, S., Katsaros, P., dan Pombortsis, A., ——-, State Space Reduction with Message Inspection in Security Protocol Model Checking, ——

Chakraborty, A., dan Garg, V. K., 2000, On Reducing the Global State Graph for Verification of Distributed Computations, —

Flanagan, C., dan Saxe, J. B., 2001, Avoiding Exponential Explosion : Generating Compact Verification Conditions, Conference Record of POPL ’01 : The 28th ACM Symposium on the Principles of Programming Language.

Godefroid, P., dan Khurshid, S., 2002, Exploring Very Large State Spaces Using Genetic Algorithms, J.-P. Katoen and P. Stevens (Eds.) : TACAS 2002, LNCS 2280, pp. 266-280, 2002.

Holzmann, G. J., 1997, The Model Checker SPIN, IEEE Transactions on Software Engineering, Vol. 23, No. 5.

Kashyap, S., dan Garg, V. K., 2001, State space reduction using Predicate Filters, NSF Grants CNS-0509024 and an Engineering Foundation Fellowship.

Sivaraj, H., dan Gopalakrishnan, G., —–, Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking, The Semiconductor Research (SRC) and the National Science Foundation (NSF).

Penelitian Sebelumnya :