2016 : DESAIN METODE ABSTRAKSI BERHINGGA PADA PETRI NET

Dr. Subiono M.Sc.
Didik Khusnul Arif S.Si, M.Si
Dieky Adzkiya S.Si, M.Si

External link

Type

RESEARCH

Keywords

-


Abstract

Petri net dapat digunakan untuk memodelkan sistem event diskrit yang mengandung sinkronisasi dan konkurensi. Di literatur, banyak metode yang dikembangkan untuk menganalisa sifat-sifat Petri net. Pada umumnya metode tersebut hanya fokus pada beberapa sifat, misalnya boundedness dan liveness. Penelitian bermaksud untuk mengembangkan hasil yang sudah ada dengan mendesain sebuah metode yang memungkinkan untuk menganalisa banyak sifat dari Petri net. Sifat-sifat tersebut diekspresikan ke dalam\nsebuah spesifikasi yang disebut linear temporal logic. Proses untuk mengetahui apakah sebuah model memenuhi sebuah spesifikasi disebut verifikasi. Ada beberapa perangkat lunak untuk melakukan verifikasi secara otomatis, misalnya SPIN, NuSMV, UPPAAL. Sayangnya kebanyakan perangkat lunak tersebut mensyaratkan agar kardinalitas dari ruang keadaan adalah berhingga. Kenyataannya kardinalitas dari ruang keadaan suatu Petri net tidak selalu berhingga. Hal ini mendorong dilakukannya penelitian untuk mendesain\nmetode abstraksi berhingga pada Petri net. Abstraksi adalah sebuah konsep fundamental yang memungkinan analisis (atau verifikasi) dari sebuah model dengan kardinalitas dari ruang keadaan yang besar atau bahkan takhingga.Jadi tujuan dari penelitian ini adalah mengembangkan sebuah metode yang memungkinkan untuk menganalisa banyak sifat dari Petri net dan proses analisa dapat dilakukan secara otomatis.