Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/59607
| Title: | การแปลงแผนภาพยูเอ็มแอลสเตทแมชชีนเป็นภาษาโพรเมลา |
| Other Titles: | Transformation of UML State Machine Diagram to Promela |
| Authors: | ปาณิสรา ดำจันทร์ |
| Advisors: | วิวัฒน์ วัฒนาวุฒิ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Advisor's Email: | Wiwat.V@Chula.ac.th,wiwatv@gmail.com,Wiwat.V@Chula.ac.th |
| Subjects: | ยูเอ็มแอล (วิทยาการคอมพิวเตอร์) UML (Computer science) |
| Issue Date: | 2560 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | การทำการทวนสอบเชิงรูปนัยโดยใช้วิธีการโมเดลเช็คกิงโดยเครื่องมือสปินนั้นต้องอาศัยแบบจำลองที่เป็นภาษาโพรเมลาซึ่งการทวนสอบเชิงรูปนัยนั้นสามารถทำได้ตั้งแต่ระยะต้นของกระบวนการพัฒนาซอฟต์แวร์โดยเฉพาะขั้นตอนการออกแบบ ปัจจุบันการออกแบบระบบได้มีการนำแผนภาพยูเอ็มแอลมาใช้โดยเฉพาะแผนภาพสเตทแมชชีนที่ช่วยอธิบายพฤติกรรมแบบพลวัตของระบบซอฟต์แวร์ วิทยานิพนธ์นี้จึงนำเสนอเครื่องมือในการแปลงแผนภาพสเตทแมชชีนที่มีการเขียนโอซีแอลไปเป็นภาษาโพรเมลา เพื่อเป็นทางเลือกหนึ่งสำหรับผู้ที่ต้องการทำการทวนสอบด้วยวิธีโมเดลเช็คกิงโดยเครื่องมือสปิน โดยวิทยานิพนธ์นี้สนใจสัญลักษณ์พื้นฐานของแผนภาพสเตทแมชชีน 5 สัญลักษณ์ด้วยกันคือ สัญลักษณ์เริ่มต้น สัญลักษณ์สิ้นสุด สัญลักษณ์สถานะ สัญลักษณ์ทางเลือก และสัญลักษณ์การเปลี่ยนสถานะ และมีแม่แบบในการแปลง 6 แม่แบบ สำหรับแปลงแผนภาพสเตทแมชชีนเป็นภาษาโพรเมลา ทั้งนี้เครื่องมือสามารถแปลงแผนภาพสเตทแมชชีนที่มีการเขียนโอซีแอลบนแผนภาพ สเตทแมชชีนไปเป็นภาษาโพรเมลาได้ โดยเครื่องมือจะรับแผนภาพสเตทแมชชีนที่อยู่ในรูปแบบแฟ้มเอกสารเอกซ์เอ็มแอลเป็นข้อมูลนำเข้าในการแปลงและข้อมูลนำออกเป็นภาษาโพรเมลา |
| Other Abstract: | 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. |
| Description: | วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2560 |
| Degree Name: | วิทยาศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิทยาศาสตร์คอมพิวเตอร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/59607 |
| URI: | http://doi.org/10.58837/CHULA.THE.2017.1259 |
| metadata.dc.identifier.DOI: | 10.58837/CHULA.THE.2017.1259 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 5870242121.pdf | 3.14 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.