Title	การทวนสอบเชิงรูปนัยของการออกแบบบีพีเอ็มเอ็นโดยใช้โมเดลเช็คกิง / ชานนท์ เดชสุภา = Formal verification of BPMN design using model checking / Chanon Dechsupa
Imprint	2561
Connect to	http://cuir.car.chula.ac.th/handle/123456789/61548
Descript	ก-ด, 169 แผ่น : ภาพประกอบ, แผนภูมิ

การทวนสอบโมเดลบีพีเอ็มเอ็นด้วยวิธีโมเดลเช็คกิงเป็นวิธีการหนึ่งที่ช่วยให้มั่นใจว่าโมเดลบีพีเอ็มเอ็นที่ออกแบบปราศจากปัญหาติดตายและปราศจากคุณสมบัติที่ไม่พึงประสงค์ที่เป็นสาเหตุโมเดลไม่ตรงตามความต้องการหรือส่งผลให้ระบบหยุดทำงาน คุณสมบัติของโมเดลบีพีเอ็มเอ็นที่จำเป็นต้องทวนสอบได้แก่ คุณสมบัติความปลอดภัยและคุณสมบัติความสมบูรณ์ ขั้นตอนการทวนสอบด้วยวิธีโมเดลเช็คกิงค่อนข้างซับซ้อนเพราะเกี่ยวข้องกับภาษารูปนัยที่ใช้อธิบายโมเดลเชิงนามธรรมและการใช้เครื่องมือทวนสอบ รวมถึงอาจต้องใช้เทคนิคเฉพาะเพื่อจัดการโมเดลบีพีเอ็มเอ็นที่มีขนาดใหญ่ที่เป็นสาเหตุของปัญหาการระเบิดของปริภูมิสถานะ การสร้างโมเดลนามธรรมโดยอัตโนมัติช่วยลดความผิดพลาดและเวลาที่ใช้ในการสร้างโมเดล สามารถจัดการโมเดลที่มีขนาดใหญ่และปัญหาการระเบิดของปริภูมิสถานะได้ งานวิจัยนี้เสนอเทคนิคการทวนสอบคุณสมบัติความปลอดภัย คุณสมบัติความสมบูรณ์ของโมเดลบีพีเอ็มเอ็นด้วยวิธีโมเดลเช็คกิง คัลเลอร์เพทริเน็ตหรือซีพีเอ็นถูกนำมาใช้อธิบายโมเดลนามธรรม เทคนิคการแบ่งโมเดลออกเป็นโมเดลย่อยและการจัดโครงสร้างโมเดลแบบมีลำดับชั้นถูกนำมาใช้เพื่อหลีกเลี่ยงปัญหาการระเบิดของปริภูมิสถานะ กรอบงานได้ถูกพัฒนาขึ้นเพื่อใช้แปลงโมเดลบีพีเอ็มเอ็นเป็นโมเดลซีพีเอ็นและมีตัวสร้างและค้นปริภูมิสถานะจากโมเดลซีพีเอ็น ซึ่งกรอบงานเป็นตัวเลือกที่มีประโยชน์สำหรับนักออกแบบกระบวนการซอฟต์แวร์ที่ต้องการทวนสอบโมเดลบีพีเอ็มเอ็นที่มีขนาดใหญ่
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