Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transforming timed uml activity diagram into timed automata
Year (A.D.)
2024
Document Type
Independent Study
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.IS.2024.289
Abstract
ในกระบวนการพัฒนาซอฟต์แวร์สมัยใหม่ที่มีความซับซ้อนสูง ความถูกต้องของระบบทั้งในเชิงฟังก์ชัน และข้อกำหนดเชิงเวลาถือเป็นปัจจัยสำคัญในการสร้างซอฟต์แวร์ที่มีคุณภาพ อย่างไรก็ตาม แผนภาพกิจกรรม ซึ่งนิยมใช้ในระยะเริ่มต้นของการออกแบบระบบ ยังขาดความสามารถในการระบุข้อจำกัดด้านเวลาโดยตรง ทำให้ไม่สามารถใช้ตรวจสอบคุณสมบัติเชิงเวลาของระบบได้อย่างครบถ้วน โครงงานมหาบัณฑิตนี้จึงมุ่งพัฒนากฎการแปลงแผนภาพกิจกรรมที่มีการกำหนดเวลาไปเป็นไทมด์ออโตมาตา ซึ่งเป็นแบบจำลองที่สามารถแสดงพฤติกรรมของระบบพร้อมข้อจำกัดเชิงเวลาได้อย่างแม่นยำ โดยจะนำแบบจำลองไทมด์ออโตมาตาที่แปลงได้เข้าสู่กระบวนการทวนสอบด้วยเครื่องมือ UPPAAL เพื่อให้สามารถตรวจสอบคุณสมบัติด้านที่ระบบจะดำเนินต่อไปจนถึงจุดหมายในอนาคต และการป้องกันข้อผิดพลาดในระบบ ได้อย่างเป็นรูปธรรม ผ่านการใช้ตรรกศาสตร์เชิงเวลาแบบต้นไม้คำนวณ ผลการทดลองแสดงให้เห็นว่า กฎการแปลงที่พัฒนาขึ้นสามารถรองรับข้อกำหนดเชิงเวลาได้อย่างเหมาะสม ในการนำไปประยุกต์ใช้ในกระบวนการพัฒนาซอฟต์แวร์แบบแอไจล์ เพื่อการออกแบบซอฟต์แวร์ที่ต้องการการควบคุมเวลาอย่างละเอียด
Other Abstract (Other language abstract of ETD)
In modern software development, where systems are increasingly complex, ensuring both functional correctness and adherence to time constraints is essential for delivering high-quality software. However, Activity Diagrams—commonly used in early stages of system design—lack the capability to directly represent time constraints. This limitation hinders their effectiveness in verifying time-dependent system properties. This master project proposes a set of transformation rules for converting time-annotated UML Activity Diagrams into Timed Automata, a formal model capable of expressing system behavior alongside temporal constraints with precision. The resulting Timed Automata models are verified using the UPPAAL tool to formally check system properties such as liveness and safety, based on Timed Computation Tree Logic. Experimental results demonstrate that the proposed transformation rules support time-based requirements and are suitable for application in agile software development processes. This contributes to the accurate design of software systems that require detailed time control.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
จันทร์หง่อม, กัญจน์วัฒน์, "การแปลงแผนภาพกิจกรรมที่มีการกำหนดเวลาเป็นไทมด์ออโตมาตา" (2024). Chulalongkorn University Theses and Dissertations (Chula ETD). 73533.
https://digital.car.chula.ac.th/chulaetd/73533