Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transforming probabilistic timed Automata to PRISM code
Year (A.D.)
2023
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.2023.296
Abstract
วิทยานิพนธ์ฉบับนี้มุ่งศึกษากระบวนการแปลงไทมด์ออโตมาตาความน่าจะเป็นเป็นรหัสปริซึม ซึ่งมีความสำคัญในการวิเคราะห์ระบบเวลาจริงและระบบที่มีความซับซ้อนด้วยความน่าจะเป็น การวิจัยนี้เสนอกฎการแปลงสำหรับแปลงไทมด์ออโตมาตาจากเอกซ์เอ็มแอลเป็นรหัสปริซึม,ช่วยในการวิเคราะห์และตรวจสอบคุณลักษณะที่ซับซ้อนของระบบ นอกจากนี้ วิทยานิพนธ์ยังได้พัฒนากระบวนการแปลงที่มีความสอดคล้องทางความหมาย ช่วยให้สามารถแปลงแบบจำลองที่ออกแบบด้วย UPPAAL ในรูปแบบเอกซ์เอ็มแอลไปยังรหัสปริซึมได้อย่างเหมาะสม ผลลัพธ์จากการศึกษานี้มีความสำคัญในการประยุกต์ใช้ทฤษฎีในแบบจำลองจริงและนำไปสู่การประยุกต์ใช้งานที่มีประสิทธิผลมากขึ้นในหลากหลายด้าน วิทยานิพนธ์ยังนำเสนอการพัฒนาเครื่องมือสำหรับการแปลงรหัสที่มีประสิทธิภาพ ซึ่งใช้ภาษาจาวาและมีความยืดหยุ่นในการปรับใช้กับระบบต่างๆ การทดสอบเครื่องมือนี้พบว่าสามารถแปลงแบบจำลองได้อย่างถูกต้องและครบถ้วน รวมถึงการจัดการกับข้อผิดพลาดที่อาจเกิดขึ้น การทดสอบครอบคลุมแสดงให้เห็นถึงความสามารถของเครื่องมือในการวิเคราะห์และทดสอบแบบจำลองที่มีความซับซ้อน ลดเวลาและความพยายามในการวิเคราะห์แบบจำลองด้วยตนเอง และทำให้มั่นใจได้ว่าผลลัพธ์ที่ได้มีความถูกต้องและเชื่อถือได้ เครื่องมือนี้มีศักยภาพในการเป็นเครื่องมือมาตรฐานสำหรับการวิเคราะห์แบบจำลองไทมด์ออโตมาตาความน่าจะเป็นในอนาคต ช่วยจัดการกับความต้องการที่ซับซ้อนของระบบในโลกจริง
Other Abstract (Other language abstract of ETD)
This dissertation focuses on studying the process of transforming timed automata probabilities into prism codes, which is important in analyzing real-time systems and complex systems with probabilities. The research proposes transformation rules for converting timed automata from XML to prism code, aiding in the analysis and verification of complex system characteristics. Additionally, the dissertation develops a semantically consistent transformation process, enabling the appropriate conversion of models designed with UPPAAL in XML format to prism code. The outcomes of this study are significant for applying theory in real-world modeling and lead to more effective applications in various fields. The thesis also presents the development of an efficient code transformation tool using Java, offering flexibility for adaptation in different systems. Testing of this tool has shown that it can accurately and completely transform models, including managing potential errors. Comprehensive testing demonstrated the tool's ability to analyze and test complex models, reducing the time and effort in manual model analysis, and ensuring the accuracy and reliability of the results. This tool has the potential to become a standard tool for analyzing probabilistic timed automata models in the future, helping to manage the complex demands of real-world systems.
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). 10248.
https://digital.car.chula.ac.th/chulaetd/10248