Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transformation of sequence diagram with state invariants into timed automata
Year (A.D.)
2023
Document Type
Independent Study
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิทยาศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิศวกรรมซอฟต์แวร์
DOI
10.58837/CHULA.IS.2023.246
Abstract
ในช่วงการออกแบบระบบหลังจากที่ได้รับความต้องการมาแล้ว และได้ผลลัพธ์ออกมาเป็นข้อตกลงตามความต้องการของระบบแล้ว แผนภาพลำดับคือส่วนสำคัญที่อธิบายถึงพฤติกรรมของระบบที่มีปฏิสัมพันธ์กัน เป็นประโยชน์มากเพื่อให้กลุ่มผู้พัฒนาเห็นการทำงานเชิงพฤติกรรมของระบบ และมองพฤติกรรมของระบบไปทิศทางเดียวกันได้ สามารถใช้ในการทวนสอบข้อตกลงของระบบว่าครบถ้วน สมบูรณ์หรือไม่ แต่แผนภาพลำดับมีปัญหาเรื่องไม่สามารถทวนสอบแบบอัตโนมัติได้ ต้องใช้การวิเคราะห์และทวนสอบโดยการตัดสินใจของมนุษย์ และพฤติกรรมในบางระบบมีรูปแบบเชิงไม่กำหนด มีความซับซ้อนและไม่สามารถทวนสอบได้ งานวิจัยนี้เล็งเห็นถึงปัญหาที่เกิดขึ้นจึงคิดวิธีการทวนสอบข้อตกลงตามความต้องการของระบบของแผนภาพลำดับ โดยใช้แบบจำลองเชิงรูปนัยชื่อ ไทม์ออโตมาตาโดยการเปรียบเทียบและวิเคราะห์โครงสร้างแผนภาพลำดับที่มีตัวยืนยงสถานะตามหลักยูเอ็มแอลเวอร์ชัน 2.0, 2.5 และเครื่องมือ UPPAAL นิยามกฎการแปลงและพัฒนาเครื่องมือสำหรับใช้ในการแปลงแผนภาพลำดับที่มีตัวยืนยงสถานะเป็นไทม์ออโตมาตา เริ่มแปลงแผนภาพลำดับที่มีตัวยืนยงสถานะด้วยแฟ้มข้อความเป็นแฟ้มเอกซ์เอ็มแอลของเครื่องมือ UPPAAL จำลองและทวนสอบไทม์ออโตมาตาตามคุณสมบัติที่สนใจที่เขียนด้วยสูตร TCTL โดยในการทดสอบเครื่องมือแปลงแผนภาพลำดับที่มีตัวยืนยงสถานะเป็นไทม์ออโตมาตากับกรณีศึกษาพบว่า สามารถช่วยให้ผู้พัฒนาระบบสามารถเห็นพฤติกรรมเชิงระบบและนำมาสู่การปรับปรุงแผนภาพให้สอดคล้องกับข้อตกลงตามความต้องการของระบบ และทวนสอบระบบได้ผลลัพธ์ออกมาน่าพึงพอใจและเป็นไปตามข้อตกลงตามความต้องการของระบบ
Other Abstract (Other language abstract of ETD)
During the system design phase, after gathering requirements, the result is the System Requirement Specification. The sequence diagram plays a crucial role in explaining the behavior of all interacting systems, which is convenient for software developers who need to visualize the system's behavior within the same context. It can be used to verify the completeness of the system requirement specification. However, the issue with the sequence diagram is that it cannot analyze and automatically verify the behavior of the system, human judgment must be used to analyze and verify it. In some systems, non-deterministic behavior may be present, making it complex and challenging to verify. We have identified this problem in the sequence diagram, leading us to define a methodology for verifying the system requirement specification of the sequence diagram using the Timed Automata formal model. We compared and analyzed the structure of the sequence diagram with state invariants from UML 2.0 and 2.5, as well as UPPAAL model checking. Furthermore, we established transformation rules and developed a transformation tool for transforming the sequence diagram with state invariants into timed automata. This involved modeling and transforming the sequence diagram with state invariants into XML format in UPPAAL, simulating and verifying it using timed computation tree logic formulas with various interesting properties. The test results of the transformation tool, based on case studies, enable software developers to visualize the system's behavior, enhance the sequence diagram in accordance with the system requirement specification, and verify the system. The results align with and satisfy the system requirement specification.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
ฐิตารีย์เดชากุล, ศุภพิชญ์ แสงมณี, "การแปลงแผนภาพลำดับที่มีตัวยืนยงสถานะเป็นไทม์ออโตมาตา" (2023). Chulalongkorn University Theses and Dissertations (Chula ETD). 11803.
https://digital.car.chula.ac.th/chulaetd/11803