Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Formal modeling of bpmn workflow for synchronous and asynchronous processes with time constraints using timed automata network
Year (A.D.)
2025
Document Type
Thesis
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Second Advisor
เนื่องวงศ์ ทวยเจริญ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิศวกรรมศาสตรดุษฎีบัณฑิต
Degree Level
ปริญญาเอก
Degree Discipline
วิศวกรรมคอมพิวเตอร์
DOI
10.58837/CHULA.THE.2025.203
Abstract
แบบจำลองบีพีเอ็มเอ็นมีบทบาทสำคัญในการออกแบบกระบวนการธุรกิจสมัยใหม่ที่มีการประมวลผลหลายส่วนพร้อมกันและรูปแบบการสื่อสารทั้งแบบซิงโครนัสและอะซิงโครนัส แต่ด้วยความเป็นแผนภาพเชิงกราฟิก บีพีเอ็มเอ็นไม่สามารถทวนสอบเชิงรูปนัยได้โดยตรง และมาตรฐานเดิมยังไม่รองรับการกำหนดข้อจำกัดช่วงเวลาให้กับกิจกรรม งานวิจัยนี้จึงเสนอการขยายบีพีเอ็มเอ็นเป็นแบบจำลองทีบีบีพี (Time-Bounded BPMN: TBBP) เพื่อรองรับการกำหนดข้อจำกัดช่วงเวลาต่ำสุด–สูงสุดของกิจกรรม พร้อมออกแบบแบบรูปสำหรับการสื่อสารแบบซิงโครนัสและอะซิงโครนัส รวมทั้งพัฒนากฎการแปลงทีบีบีพีไปเป็นไทมด์ออโตมาตาเพื่อทวนสอบด้วย UPPAAL และกฎการแปลงข้อคำถามจากตรรกศาสตร์เชิงเวลาแบบเมตริก (MTL) ไปเป็นตรรกศาสตร์เชิงเวลาแบบต้นไม้คำนวณแบบมีเงื่อนไขเวลา (TCTL) นอกจากนี้ได้พัฒนาเครื่องมือ TBBPTA Tool เพื่อแปลงไฟล์บีพีเอ็มเอ็น (XML) เป็นแบบจำลองไทมด์ออโตมาตา (XML) ที่สามารถนำเข้าสู่ UPPAAL เพื่อทวนสอบได้โดยอัตโนมัติ
Other Abstract (Other language abstract of ETD)
BPMN models play a crucial role in designing modern business processes that involve parallel execution and both synchronous and asynchronous communication. However, because BPMN provides only a graphical representation, it cannot be directly subjected to formal verification, and the standard does not support specifying time constraints for tasks or other process elements. This research proposes an extension of BPMN, called Time-Bounded BPMN (TBBP), which allows specifying minimum–maximum time bounds for activities and introduces patterns for synchronous and asynchronous communication to capture typical interaction mechanisms in business processes. Transformation rules are defined to transform TBBP models into Timed Automata for verification with UPPAAL, along with rules for transforming Metric Temporal Logic (MTL) queries into Timed Computational Tree Logic (TCTL). Furthermore, the TBBPTA Tool is developed to automatically transform BPMN XML files into Timed Automata XML models that can be directly imported into UPPAAL for formal verification.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
เขตรการณ์, กิตติศักดิ์, "การสร้างแบบจำลองเชิงรูปนัยของกระแสงานบีพีเอ็มเอ็นสำหรับกระบวนการซิงโครนัสและอะซิงโครนัสที่มีข้อจำกัดช่วงเวลาโดยใช้เครือข่ายไทมด์ออโตมาตา" (2025). Chulalongkorn University Theses and Dissertations (Chula ETD). 75497.
https://digital.car.chula.ac.th/chulaetd/75497