Office of Academic Resources
Chulalongkorn University
Chulalongkorn University

Home / Help

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

SUMMARY

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


การรื้อปรับระบบ วิศวกรรมซอฟต์แวร์ Reengineering (Management) Software engineering ปริญญาดุษฎีบัณฑิต



Location



Office of Academic Resources, Chulalongkorn University, Phayathai Rd. Pathumwan Bangkok 10330 Thailand

Contact Us

Tel. 0-2218-2929,
0-2218-2927 (Library Service)
0-2218-2903 (Administrative Division)
Fax. 0-2215-3617, 0-2218-2907

Social Network

  line

facebook   instragram