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.

Share

COinS
 
 

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.