VERIFIKASI FORMAL PETRI NET DENGAN COUNTER PADA SISTEM INVENTORI

PERTIIWI, RUVITA IFFAHTUR (2016) VERIFIKASI FORMAL PETRI NET DENGAN COUNTER PADA SISTEM INVENTORI. Masters thesis, Institut Teknologi Sepuluh Nopember.

Preview	Text 1214201202-Abstract.pdf - Published Version Download (163kB) | Preview
Preview	Text 1214201202-Conclusion.pdf - Published Version Download (184kB) | Preview
Preview	Text 1214201202-Master_Theses.pdf - Published Version Download (1MB) | 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:	Thesis (Masters)
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/297

Actions (login required)

View Item