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.)


Document Type


First Advisor

วิวัฒน์ วัฒนาวุฒิ


Faculty of Engineering (คณะวิศวกรรมศาสตร์)

Department (if any)

Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)

Degree Name


Degree Level


Degree Discipline





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



To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.