ABSTRAK
Fakultas Informatika Telkom University menyelenggarakan Tugas Akhir (TA) untuk mahasiswa yang akan menentukan kelulusan. Dalam Tugas Akhir menggunakan proses bisnis untuk jalannya proses sehingga seluruh proses dapat terstruktur. Dalam hal ini proses bisnis Tugas Akhir sebaiknya dimodelkan dalam Business Process Modeling Notation (BPMN). Spesifikasi dari BPMN tidak memasukkan formal semantics. Kekurangan dari formal semantics membuat kesulitan dalam mengecek correctness dan kelengkapan BPMN dari segi semantics prespective. Sehingga tidak bisa mengecek correctness dari proses bisnis TA. Dibutuhkan pendekatan dengan menejermahkan model Business Process Modeling Notation (BPMN) ke Petri Net. Hasil konversi yang telah berbetuk Petri Net kemudian diverifikasi dengan beberapa tools yang terdapat di Petri Net yaitu Woflan. Verifikasi digunakan untuk mendeteksi seperti deadlocks and livelocks BPMN yang telah dimodelkan ke dalam Petri Net. Analisis yang dilakukan adalah selain mendiagnosis proses bisnis TA, juga dilakukan modifikasi proses pengujian terhadap informal semantics BPMN seperti exclusive gateway, activities, event. Dari hasil diagnosis didapatkan bahwa properti pada Petri Net dapat digunakan untuk melakukan verifikasi proses bisnis. Selain itu dari kelengkapan proses bisnis BPMN, ketika salah satu informal semanticts dihilangkan contohnya exclusive gateway, maka ketika dilakukan diagnosis ternyata workflow tersebut tidak sound. Juga ketika dilakukan penambahan intermediate ternyata didapatkan hasil diagnosis bahwa workflow tetap sound.
Kata Kunci : Petri Net,Woflan, BPMN