Pemodelan proses bisnis merupakan salah satu metode yang populer untuk meningkatkan kualitas dan efisiensi dalam organisasi. Business Process Modelling Notation (BPMN) merupakan standar pemodelan proses bisnis pada fase awal pembangunan sistem. BPMN memiliki berbagai keunggulan, diantaranya modelnya mudah dipahami oleh pengguna, dan dapat meminimalisir adanya kesenjangan antara proses perancangan dan implementasi sistem. Disamping kelebihannya, BPMN memiliki beberapa kekurangan dalam pemodelan proses bisnis, diantaranya yaitu ambiguitas pada spesifikasi standar yang sudah ditetapkan, serta kompleksitas bahasa yang dibentuk sehingga perlu dibuat formalisasi model BPMN untuk mengurangi kompleksitas bahasa dan menangani isu ambiguitas pada spesifikasi standar. Salah satu usaha untuk melakukan formalisasi model BPMN adalah dengan melakukan transformasi model BPMN ke Petri net.
Petri net merupakan alat pemodelan grafis dan matematis berbasis graf bipartit yang berarah dan dapat diaplikasikan pada banyak sistem yang mudah dipahami oleh praktisi dalam mengimplementasikan model petri net, maupun ilmuan dalam pemodelan matematisnya. Untuk melakukan transformasi dari model BPMN ke Petri net, perlu dilakukan formalisasi model dan memerlukan aturan transformasi sesuai metode Dijkman dalam proses transformasi model BPMN ke Petri net. Tugas akhir ini bertujuan untuk mengaplikasikan metode Dijkman untuk transformasi model BPMN ke Petri net serta analisisnya.
Hasil penelitian ini menunjukkan bahwa jumlah end event dalam satu model BPMN berpengaruh terhadap liveness dari model Petri net yang dibentuk. Jika suatu model BPMN memiliki lebih dari satu end event, maka model Petri net hasil transformasinya tidak memenuhi kriteria liveness. Hasil lain menunjukkan bahwa perulangan (loop) pada model BPMN yang menggunakan XOR gateway tidak menimbulkan adanya unbounded place pada model Petri net yang dibentuk.
Kata Kunci : Transformasi, BPMN, Petri net, Dijkman, Analisis Formal, Proses Bisnis