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...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item PeerReviewed |
| Language: | English |
| Published: |
2014
|
| Subjects: | |
| Online Access: | https://repository.ugm.ac.id/37639/1/DP-H%40DFEx-14.pdf https://repository.ugm.ac.id/37639/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | 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. |
|---|