Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transformation of a concurrent state machine diagram into NuSMV
Year (A.D.)
2024
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.2024.24
Abstract
ระบบเชิงพร้อมกันเป็นระบบที่มีมากกว่าหนึ่งสายโยงใยซึ่งสามารถสลับกันทำงานระหว่างสายโยงใยโดยที่ไม่ต้องรอให้กระบวนการในสายโยงใยใดกระบวนการหนึ่งให้เสร็จสมบูรณ์ ซึ่งระบบเชิงพร้อมกันมักพบในระบบที่มีความซับซ้อน มีหลายงานที่ต้องดำเนินการและสายโยงใยที่ดำเนินงานนั้นอาจมีปฏิสัมพันธ์กัน เช่น เข้าถึงหน่วยความจำเดียวกัน เป็นต้น หนึ่งในวิธีที่สามารถอธิบายระบบเชิงพร้อมกันคือการใช้แผนภาพเครื่องสถานะซึ่งเป็นแผนภาพตามมาตรฐานยูเอ็มแอลรุ่น 2.5 แต่เนื่องจากแผนภาพเครื่องสถานะของระบบเชิงพร้อมกันไม่สามารถนำมาใช้ในการทวนสอบได้ เนื่องจากพฤติกรรมของระบบเชิงพร้อมกันมีรูปแบบเชิงไม่กำหนด งานวิจัยจึงเล็งเห็นประโยชน์ในการพัฒนาเครื่องมือแปลงแผนภาพเครื่องสถานะเป็นโค้ดนูเอ็สเอ็มวี ซึ่งเป็นการแปลงแผนภาพเครื่องสถานะของระบบเชิงพร้อมกันให้อยู่ในรูปของแบบจำลองเชิงรูปนัยให้สามารถทำการทวนสอบได้ โดยเปรียบเทียบและวิเคราะห์ระหว่างองค์ประกอบของแผนภาพเครื่องสถานะของระบบเชิงพร้อมกันตามมาตรฐานยูเอ็มแอลรุ่น 2.5 กับองค์ประกอบของนูเอ็สเอ็มวี แล้วนิยามกฏการแปลงแผนภาพเครื่องสถานะของระบบเชิงพร้อมกันให้เป็นนูเอ็สเอ็มวีเพื่อใช้ในการพัฒนาเครื่องมือการแปลง จากนั้นจึงพัฒนาเครื่องมือการแปลง สร้างแบบจำลองซึ่งเป็นกรณีศึกษาของระบบเชิงพร้อมกันที่อยู่ในรูปของแผนภาพเครื่องสถานะ สร้างข้อกำหนดเชิงรูปนัยที่ใช้ในการทวนสอบกรณีศึกษา และนำเครื่องมือการแปลงมาใช้ในการแปลงแบบจำลองกรณีศึกษาให้เป็นแบบจำลองเชิงรูปนัยนูเอ็สเอ็มวี แล้วทำการทวนสอบด้วยข้อกำหนดเชิงรูปนัยบนนูเอ็มเอ็มวี กระบวนการวิจัยและพัฒนาทั้งหมดที่กล่าวมาพบว่าผู้วิจัยสามารถแปลงแบบจำลองในรูปของแผนภาพเครื่องสถานะให้ป็นแบบจำลองเชิงรูปนัยและเห็นพฤติกรรมของการทำงานของระบบเชิงพร้อมกัน รวมถึงทวนสอบพฤติกรรมของระบบและได้ผลลัพธ์จากการทวนสอบที่เป็นไปตามข้อกำหนดเชิงรูปนัย
Other Abstract (Other language abstract of ETD)
Concurrent systems are systems that have more than one thread, allowing for switching between threads without waiting for the processes in any one thread to complete. These systems are often found in complex environments with multiple tasks to perform, where the threads executing these tasks may interact with each other—for example, accessing the same memory unit. One method to describe concurrent systems is by using state machine diagrams conforming to the UML 2.5 standard. However, state machine diagrams of concurrent systems cannot be used for verification because the behavior of concurrent systems is non-deterministic. This research recognizes the benefit of developing a tool to transform state machine diagrams into NuSMV code, effectively converting the state machine diagrams of concurrent systems into formal models that can be verified. By comparing and analyzing the components of state machine diagrams of concurrent systems according to the UML 2.5 standard with the components of NuSMV, we define translation rules to convert these diagrams into NuSMV for translator development. Subsequently, researcher develops the transformation tool, create a model as a case study of a concurrent system in the form of a state machine diagram, and formulate formal specifications used to verify the case study. Researcher then apply the transformation tool to convert the case study model into a formal NuSMV model and perform verification using the formal specifications on NuSMV. The entire research and development process demonstrates that the researcher can transform models in the form of state machine diagrams into formal models and observes the behavior of concurrent system operations. This includes verifying system behavior and obtaining verification results that satisfy to the formal specifications.
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). 11801.
https://digital.car.chula.ac.th/chulaetd/11801
