Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transformation of UML State Machine Diagram to Promela
Year (A.D.)
2017
Document Type
Thesis
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิทยาศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิทยาศาสตร์คอมพิวเตอร์
DOI
10.58837/CHULA.THE.2017.1259
Abstract
การทำการทวนสอบเชิงรูปนัยโดยใช้วิธีการโมเดลเช็คกิงโดยเครื่องมือสปินนั้นต้องอาศัยแบบจำลองที่เป็นภาษาโพรเมลาซึ่งการทวนสอบเชิงรูปนัยนั้นสามารถทำได้ตั้งแต่ระยะต้นของกระบวนการพัฒนาซอฟต์แวร์โดยเฉพาะขั้นตอนการออกแบบ ปัจจุบันการออกแบบระบบได้มีการนำแผนภาพยูเอ็มแอลมาใช้โดยเฉพาะแผนภาพสเตทแมชชีนที่ช่วยอธิบายพฤติกรรมแบบพลวัตของระบบซอฟต์แวร์ วิทยานิพนธ์นี้จึงนำเสนอเครื่องมือในการแปลงแผนภาพสเตทแมชชีนที่มีการเขียนโอซีแอลไปเป็นภาษาโพรเมลา เพื่อเป็นทางเลือกหนึ่งสำหรับผู้ที่ต้องการทำการทวนสอบด้วยวิธีโมเดลเช็คกิงโดยเครื่องมือสปิน โดยวิทยานิพนธ์นี้สนใจสัญลักษณ์พื้นฐานของแผนภาพสเตทแมชชีน 5 สัญลักษณ์ด้วยกันคือ สัญลักษณ์เริ่มต้น สัญลักษณ์สิ้นสุด สัญลักษณ์สถานะ สัญลักษณ์ทางเลือก และสัญลักษณ์การเปลี่ยนสถานะ และมีแม่แบบในการแปลง 6 แม่แบบ สำหรับแปลงแผนภาพสเตทแมชชีนเป็นภาษาโพรเมลา ทั้งนี้เครื่องมือสามารถแปลงแผนภาพสเตทแมชชีนที่มีการเขียนโอซีแอลบนแผนภาพ สเตทแมชชีนไปเป็นภาษาโพรเมลาได้ โดยเครื่องมือจะรับแผนภาพสเตทแมชชีนที่อยู่ในรูปแบบแฟ้มเอกสารเอกซ์เอ็มแอลเป็นข้อมูลนำเข้าในการแปลงและข้อมูลนำออกเป็นภาษาโพรเมลา
Other Abstract (Other language abstract of ETD)
Formal verification using model checking with SPIN needs a formal model written in Promela. However, the formal verification would be conducted in the early phase of software development process, especially in the design phase. Nowadays, the system design commonly uses UML diagrams, especially, the state machine diagram that describes the dynamic behavior of the software system. This thesis proposes an automatic tool to translate a UML state machine diagram along with OCL into Promela code, in order to be an alternative model for verification in model checking method with SPIN. This thesis considers mainly on five elements of the diagram, including initial state, final state, state, choice, and transition. We provide five mapping rules and six mapping templates are provided for transforming a state machine to Promela code. The software tool is developed to perform the translation of the state machine diagram with OCL into Promela code. The input state machine is expected in XML format and the output is generated in Promela code.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
ดำจันทร์, ปาณิสรา, "การแปลงแผนภาพยูเอ็มแอลสเตทแมชชีนเป็นภาษาโพรเมลา" (2017). Chulalongkorn University Theses and Dissertations (Chula ETD). 1749.
https://digital.car.chula.ac.th/chulaetd/1749