VERIFIKASI FORMAL PETRI NET DENGAN COUNTER PADA SISTEM INVENTORI

PERTIIWI, RUVITA IFFAHTUR (2016) VERIFIKASI FORMAL PETRI NET DENGAN COUNTER PADA SISTEM INVENTORI. In: Tugas Akhir.

[img]
Preview
Text
1214201202-Paper.pdf - Published Version

Download (642kB) | Preview
[img]
Preview
Text
1214201202-Presentasi.pdf - Published Version

Download (638kB) | Preview

Abstract

Verifikasi formal merupakan cara untuk memeriksa apakah sistem memenuhi spesifikasi atau tidak. Petri net dengan counter (PNZ) merupakan salah satu alat untuk memodelkan sistem event diskrit yang dilengkapi representasi data dengan variabel-variabelnya adalah bilangan bulat. Pada penelitian ini dikonstruksi PNZ dari suatu sistem inventori. Pada sistem ini Agen melakukan pembelian barang dan penjualan barang dengan terdapat dua barang yaitu barang A dan barang B. Variabel-variabel dan konstanta pada sistem inventori ini merupakan bilangan bulat tak negatif. Model PNZ sistem inventori pada penelitian ini memiliki state tak berhingga, sehingga tidak bisa diverifikasi dengan software. Agar verifikasi bisa dilakukan dengan software, digunakan metode abstraksi berhingga. Abstraksi berhingga membuat sistem dengan state tak berhingga (pada sistem transisi kongkrit) menjadi berhingga (pada sistem transisi abstrak). Verifikasi formal membutuhkan spesifikasi formal, dimana spesifikasi formal yang sesuai untuk permasalahan pada penelitian ini adalah Linear Temporal Logic (LTL). Jika sistem transisi abstrak memenuhi spesifikasi, maka sistem transisi kongkrit juga memenuhi spesifikasi. Beberapa spesifikasi yang diberikan pada penelitian ini antara lain yang pertama yaitu ”pada transaksi berikutnya Agen selalu mendapat keuntungan”, spesifikasi yang kedua, ”pada suatu waktu barang A selalu ada dalam gudang”, spesifikasi ketiga ”pada suatu waktu, akhirnya Agen memperoleh keuntungan dan tersedianya barang A dalam gudang”, dan spesifikasi keempat ”pada saat Agen tidak mendapat keuntungan tetapi memiliki barang A dalam gudang, maka akhirnya Agen dapat memperoleh keuntungan”. Pada penelitian ini software yang digunakan untuk verifikasi adalah NuSMV.

Item Type: Conference or Workshop Item (Paper)
Uncontrolled Keywords: Petri net dengan counter, verifikasi formal, spesifikasi formal, LTL, abstraksi berhingga, sistem inventori, NuSMV.
Subjects: Q Science > QA Mathematics
Q Science > QA Mathematics > QA75 Electronic computers. Computer science. EDP
Divisions: Faculty of Engineering, Science and Mathematics > School of Engineering Sciences
Depositing User: RUVITA IFFAHTUR PERTIWI
Date Deposited: 15 Jun 2016 17:46
Last Modified: 27 Dec 2018 03:36
URI: http://repository.its.ac.id/id/eprint/298

Actions (login required)

View Item View Item