Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Formal verification of BPMN design using model checking
Year (A.D.)
2018
Document Type
Thesis
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิศวกรรมศาสตรดุษฎีบัณฑิต
Degree Level
ปริญญาเอก
Degree Discipline
วิศวกรรมคอมพิวเตอร์
DOI
10.58837/CHULA.THE.2018.1253
Abstract
การทวนสอบโมเดลบีพีเอ็มเอ็นด้วยวิธีโมเดลเช็คกิงเป็นวิธีการหนึ่งที่ช่วยให้มั่นใจว่าโมเดลบีพีเอ็มเอ็นที่ออกแบบปราศจากปัญหาติดตายและปราศจากคุณสมบัติที่ไม่พึงประสงค์ที่เป็นสาเหตุโมเดลไม่ตรงตามความต้องการหรือส่งผลให้ระบบหยุดทำงาน คุณสมบัติของโมเดลบีพีเอ็มเอ็นที่จำเป็นต้องทวนสอบได้แก่ คุณสมบัติความปลอดภัยและคุณสมบัติความสมบูรณ์ ขั้นตอนการทวนสอบด้วยวิธีโมเดลเช็คกิงค่อนข้างซับซ้อนเพราะเกี่ยวข้องกับภาษารูปนัยที่ใช้อธิบายโมเดลเชิงนามธรรมและการใช้เครื่องมือทวนสอบ รวมถึงอาจต้องใช้เทคนิคเฉพาะเพื่อจัดการโมเดลบีพีเอ็มเอ็นที่มีขนาดใหญ่ที่เป็นสาเหตุของปัญหาการระเบิดของปริภูมิสถานะ การสร้างโมเดลนามธรรมโดยอัตโนมัติช่วยลดความผิดพลาดและเวลาที่ใช้ในการสร้างโมเดล สามารถจัดการโมเดลที่มีขนาดใหญ่และปัญหาการระเบิดของปริภูมิสถานะได้ งานวิจัยนี้เสนอเทคนิคการทวนสอบคุณสมบัติความปลอดภัย คุณสมบัติความสมบูรณ์ของโมเดลบีพีเอ็มเอ็นด้วยวิธีโมเดลเช็คกิง คัลเลอร์เพทริเน็ตหรือซีพีเอ็นถูกนำมาใช้อธิบายโมเดลนามธรรม เทคนิคการแบ่งโมเดลออกเป็นโมเดลย่อยและการจัดโครงสร้างโมเดลแบบมีลำดับชั้นถูกนำมาใช้เพื่อหลีกเลี่ยงปัญหาการระเบิดของปริภูมิสถานะ กรอบงานได้ถูกพัฒนาขึ้นเพื่อใช้แปลงโมเดลบีพีเอ็มเอ็นเป็นโมเดลซีพีเอ็นและมีตัวสร้างและค้นปริภูมิสถานะจากโมเดลซีพีเอ็น ซึ่งกรอบงานเป็นตัวเลือกที่มีประโยชน์สำหรับนักออกแบบกระบวนการซอฟต์แวร์ที่ต้องการทวนสอบโมเดลบีพีเอ็มเอ็นที่มีขนาดใหญ่
Other Abstract (Other language abstract of ETD)
Formal verification using model checking is a process to ensure that the BPMN design model is free of deadlock and other undesirable properties that can cause a system crash. Safeness and soundness are the important properties that have to be verified of the BPMN design model. Formal verification is a complicated procedure involving the fomal language for model abstraction and the use of model checking tools, including the techniques for handling large-scale BPMN design model and state space explosion problem. An automated transformation can reduce the flaws, time consumption, and complexity of the large-scale BPMN design mode, as well as overcoming the state space explosion problem. This paper proposes the safeness and soundness verification techniques for BPMN design model using model checking. Colored Petri Net (CPN) is used to describe an abstract model. A BPMN partitioning technique and a hierarchical verification are used for avoiding state space explosion problem. To validate and analyze BPMN design model, the transformation technique and state space generator have been implemented as a BPMN verification framework which is a viable option for the software process designers and suitable for large-scale BPMN design model verification.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
เดชสุภา, ชานนท์, "การทวนสอบเชิงรูปนัยของการออกแบบบีพีเอ็มเอ็นโดยใช้โมเดลเช็คกิง" (2018). Chulalongkorn University Theses and Dissertations (Chula ETD). 3384.
https://digital.car.chula.ac.th/chulaetd/3384