Verifikasi Command Transfer Protocol Menggunakan SPIN

Formal verification adalah metode untuk membuktikan bahwa sebuah implementasi betul-betul mengimplementasikan apa yang dijabarkan dalam bentuk spesifikasinya. Model checking merupakan salah satu metode formal verification. Model checking merupakan salah satu cabang metode formal. Penerapan model che...

وصف كامل

محفوظ في:
التفاصيل البيبلوغرافية
المؤلفون الرئيسيون: Dewi, Ervin Kusuma, Pulungan, Reza
التنسيق: Conference or Workshop Item PeerReviewed
اللغة:English
منشور في: 2014
الموضوعات:
الوصول للمادة أونلاين:https://repository.ugm.ac.id/37639/1/DP-H%40DFEx-14.pdf
https://repository.ugm.ac.id/37639/
الوسوم: إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
المؤسسة: Universitas Gadjah Mada
اللغة: English
الوصف
الملخص:Formal verification adalah metode untuk membuktikan bahwa sebuah implementasi betul-betul mengimplementasikan apa yang dijabarkan dalam bentuk spesifikasinya. Model checking merupakan salah satu metode formal verification. Model checking merupakan salah satu cabang metode formal. Penerapan model checking secara umum memerlukan tiga tahapan, yaitu pemodelan, formalisasi properti dan verifikasi. Pemodelan protokol dilakukan dengan menggunakan bahasa PROMELA, sedangkan formalisasi properti dilakukan dengan menggunakan LTL (Linear Temporal Logic). Model dan properti formal yang dihasilkan menjadi masukan untuk tool verifier SPIN. Tujuan penelitian ini adalah memodelkan sebuah protokol dalam PROMELA dan kemudian memverifikasinya dengan menggunakan SPIN. Penelitian ini menggunakan kasus protokol Command Transfer Protocol (CTP) yang dikembangkan oleh Lev Naumov. Terdapat sembilan properti yang akan dicek. Hasil verifikasi protokol menunjukkan bahwa kesembilan properti tersebut terpenuhi.