Please use this identifier to cite or link to this item: http://cuir.car.chula.ac.th/handle/123456789/61548
Title: การทวนสอบเชิงรูปนัยของการออกแบบบีพีเอ็มเอ็นโดยใช้โมเดลเช็คกิง
Other Titles: Formal verification of BPMN design using model checking
Authors: ชานนท์ เดชสุภา
Advisors: วิวัฒน์ วัฒนาวุฒิ
Other author: จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
Issue Date: 2561
Publisher: จุฬาลงกรณ์มหาวิทยาลัย
Abstract: การทวนสอบโมเดลบีพีเอ็มเอ็นด้วยวิธีโมเดลเช็คกิงเป็นวิธีการหนึ่งที่ช่วยให้มั่นใจว่าโมเดลบีพีเอ็มเอ็นที่ออกแบบปราศจากปัญหาติดตายและปราศจากคุณสมบัติที่ไม่พึงประสงค์ที่เป็นสาเหตุโมเดลไม่ตรงตามความต้องการหรือส่งผลให้ระบบหยุดทำงาน คุณสมบัติของโมเดลบีพีเอ็มเอ็นที่จำเป็นต้องทวนสอบได้แก่ คุณสมบัติความปลอดภัยและคุณสมบัติความสมบูรณ์ ขั้นตอนการทวนสอบด้วยวิธีโมเดลเช็คกิงค่อนข้างซับซ้อนเพราะเกี่ยวข้องกับภาษารูปนัยที่ใช้อธิบายโมเดลเชิงนามธรรมและการใช้เครื่องมือทวนสอบ รวมถึงอาจต้องใช้เทคนิคเฉพาะเพื่อจัดการโมเดลบีพีเอ็มเอ็นที่มีขนาดใหญ่ที่เป็นสาเหตุของปัญหาการระเบิดของปริภูมิสถานะ การสร้างโมเดลนามธรรมโดยอัตโนมัติช่วยลดความผิดพลาดและเวลาที่ใช้ในการสร้างโมเดล สามารถจัดการโมเดลที่มีขนาดใหญ่และปัญหาการระเบิดของปริภูมิสถานะได้ งานวิจัยนี้เสนอเทคนิคการทวนสอบคุณสมบัติความปลอดภัย คุณสมบัติความสมบูรณ์ของโมเดลบีพีเอ็มเอ็นด้วยวิธีโมเดลเช็คกิง คัลเลอร์เพทริเน็ตหรือซีพีเอ็นถูกนำมาใช้อธิบายโมเดลนามธรรม เทคนิคการแบ่งโมเดลออกเป็นโมเดลย่อยและการจัดโครงสร้างโมเดลแบบมีลำดับชั้นถูกนำมาใช้เพื่อหลีกเลี่ยงปัญหาการระเบิดของปริภูมิสถานะ กรอบงานได้ถูกพัฒนาขึ้นเพื่อใช้แปลงโมเดลบีพีเอ็มเอ็นเป็นโมเดลซีพีเอ็นและมีตัวสร้างและค้นปริภูมิสถานะจากโมเดลซีพีเอ็น ซึ่งกรอบงานเป็นตัวเลือกที่มีประโยชน์สำหรับนักออกแบบกระบวนการซอฟต์แวร์ที่ต้องการทวนสอบโมเดลบีพีเอ็มเอ็นที่มีขนาดใหญ่
Other Abstract: 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.
Description: วิทยานิพนธ์ (วศ.ด.)--จุฬาลงกรณ์มหาวิทยาลัย, 2561
Degree Name: วิศวกรรมศาสตรดุษฎีบัณฑิต
Degree Level: ปริญญาเอก
Degree Discipline: วิศวกรรมคอมพิวเตอร์
URI: http://cuir.car.chula.ac.th/handle/123456789/61548
Type: Thesis
Appears in Collections:FACULTY OF ENGINEERING

Files in This Item:
File Description SizeFormat 
5771463621.pdf7.5 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.