Febryanto, Kurnia Cahya (2026) Pendekatan Formal Untuk Analisis Business Process Model Notation Tipe Kolaborasi Berbasis Graf. Masters thesis, Institut Teknologi Sepuluh Nopember.
|
Text
6025241065-Master_Thesis.pdf Restricted to Repository staff only Download (9MB) | Request a copy |
Abstract
Business Process Model and Notation (BPMN) merupakan standar internasional untuk memodelkan proses bisnis secara visual. Namun, model BPMN dapat mengandung kesalahan struktural seperti deadlock dan livelock yang menghambat eksekusi proses bisnis. Penelitian ini mengembangkan kerangka kerja analisis berbasis graf yang terintegrasi dengan Linear Temporal Logic (LTL) untuk mendeteksi dan memverifikasi kesalahan struktural pada model BPMN kolaboratif melalui lima tahap metodologi. Tahap pertama mengimplementasikan Multi-Criteria Detection Algorithm untuk transformasi model dari berbagai format ke representasi graf. Tahap kedua mengembangkan formula LTL untuk mendeteksi 13 varian kesalahan dalam empat kategori yaitu improper structuring deadlock, loop deadlock, source deadlock, dan conditional livelock. Tahap ketiga melakukan analisis graf melalui metrik sentralitas, reachability, dan pencocokan pola struktural. Tahap keempat menerapkan pengayaan semantik berbasis Natural Language Processing untuk validasi konvensi penamaan. Tahap kelima menghasilkan rekomendasi perbaikan. Evaluasi dilakukan terhadap 127 model BPMN kolaboratif yang menunjukkan coverage transformasi 99,30%, F1-score deteksi kesalahan 84,93%, dan akurasi deteksi pola graf 93,48%. Perbandingan dengan metode existing menunjukkan peningkatan accuracy sebesar 3,82% dengan coverage deteksi 87,14%. Secara keseluruhan, metodologi mencapai rata-rata performa 89,19%.
===============================================================================================================================
Business Process Model and Notation (BPMN) is an international standard for visually modeling business processes. However, BPMN models may contain structural errors such as deadlocks and livelocks that hinder the execution of business processes. This research develops a graph-based analysis framework integrated with Linear Temporal Logic (LTL) to detect and verify structural errors in collaborative BPMN models through a five-stage methodology. The first stage implements a Multi-Criteria Detection Algorithm to transform models from various formats into graph representations. The second stage develops LTL formulas to detect 13 error variants across four categories: improper structuring deadlock, loop deadlock, source deadlock, and conditional livelock. The third stage performs graph analysis through centrality metrics, reachability, and structural pattern matching. The fourth stage applies semantic enrichment based on Natural Language Processing for naming convention validation. The fifth stage generates repair recommendations. Evaluation was conducted on 127 collaborative BPMN models, demonstrating a transformation coverage of 99.30%, an F1-score for error detection of 84.93%, and a graph pattern detection accuracy of 93.48%. Comparison with existing methods shows an accuracy improvement of 3.82% with a detection coverage o
| Item Type: | Thesis (Masters) |
|---|---|
| Uncontrolled Keywords: | Linear Temporal Logic, Livelock, Verifikasi Formal , BPMN, Deadlock, Formal Verification, Graph, Linear Temporal Logic, Livelock |
| Subjects: | Q Science > QA Mathematics > QA166 Graph theory Q Science > QA Mathematics > QA401 Mathematical models. Q Science > QA Mathematics > QA76 Computer software |
| Divisions: | Faculty of Intelligent Electrical and Informatics Technology (ELECTICS) > Informatics Engineering > 55101-(S2) Master Thesis |
| Depositing User: | Kurnia Cahya Febryanto |
| Date Deposited: | 29 Jan 2026 07:54 |
| Last Modified: | 29 Jan 2026 07:54 |
| URI: | http://repository.its.ac.id/id/eprint/130392 |
Actions (login required)
![]() |
View Item |
