Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
State Space Generator for LTL Model Checking using LSTM with Multi-Label Classification
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.295
Abstract
กระบวนการทวนสอบเชิงรูปนัยเป็นสิ่งที่สำคัญในการตรวจสอบความปลอดภัย ความดำเนินชีวิตและความสัมพันธ์ของระบบซอฟต์แวร์ตั้งแต่เริ่มต้นออกแบบซอฟต์แวร์ ซึ่งสามารถช่วยให้ลดความพยายามในการพัฒนาอย่างเห็นได้ชัด โมเดลเช็กกิงเป็นวิธีการเชิงรูปนัยอย่างหนึ่งที่สามารถทวนสอบระบบซอฟต์แวร์ตามคุณสมบัติเชิงพฤติกรรมที่เขียนเป็นสูตรตรรกศาสตร์เชิงเวลาแบบลำดับหรือเรียกว่าสูตรแอลทีแอล โดยใช้วิธีการสำรวจเส้นทางดำเนินงานที่เป็นไปได้ทั้งหมดอย่างละเอียดถี่ถ้วนในปริภูมิสถานะของระบบซอฟต์แวร์และกำหนดว่าเส้นทางดำเนินงานทั้งหมดของระบบเป็นไปตามคุณสมบัติที่เขียนโดยใช้สูตรแอลทีแอลหรือไม่ อย่างไรก็ตาม ระบบที่มีขนาดใหญ่และมีความซับซ้อนอาจทำให้เกิดการระเบิดของปริภูมิสถานะในการทำโมเดลเช็กกิงได้ ซึ่งมีการเสนอวิธีการลดพื้นที่ของปริภูมิสถานะหลายวิธีและแม้แต่วิธีการของแมชชีนเลิร์นนิงก็ถูกนำมาใช้เพื่อทำนายผลลัพธ์ความพึงพอใจของคุณสมบัติแอลทีแอลของระบบซอฟต์แวร์ เมื่อพิจารณาถึงความสำเร็จในการฝึกอบรมโครงข่ายความจำระยะสั้นแบบยาวหรือแอลเอสทีเอ็มสำหรับการทำนายลำดับข้อมูลอนุกรมเวลาแบบยาว ในวิทยานิพนธ์นี้ ได้เสนอแนวคิดแอลเอสทีเอ็มที่ขยายการจำแนกแบบหลายป้ายและกลยุทธ์การหาขีดแบ่งเพื่อบรรเทาปัญหาการระเบิดของปริภูมิสถานะและสร้างเป็นเครื่องสร้างปริภูมิสถานะสำหรับสร้างเส้นทางดำเนินงานของระบบซอฟต์แวร์ได้ตามที่ต้องการ โดย ได้สร้างเครื่องมือในการทวนสอบคุณสมบัติพื้นฐานของระบบซอฟต์แวร์ ได้แก่ คุณสมบัติด้านความปลอดภัย ด้านความดำเนินชีวิตและด้านความสัมพันธ์ ด้วยเทคนิคออน-เดอะ-ฟลาย
Other Abstract (Other language abstract of ETD)
The formal verification process is important for verifying the safety, liveness and correlation of a software system from the very beginning of its software design. This obviously helps decrease development efforts. Model checking is a formal method exploited to verify a given software system against target behavioral properties written in linear temporal logic (LTL) formulas. It exhaustively explores all possible execution paths in the state space of the given software system and determines whether all execution paths satisfy the target LTL properties. However, the huge size and complexity of the software system occasionally cause the state space explosion problem in model checking. Several state space reduction methods have been proposed, and even the machine learning approach is exploited to predict the LTL property satisfaction of the software system. Considering the successful training of Long Short-Term Memory (LSTM) networks for predicting long sequences of time series data. In this dissertation, an extension of LSTM with multi-label classification and a threshold strategy is proposed to mitigate the state space explosion problem and implement the state space generator for generating execution paths of the given software system on-demand. This dissertation has developed a verification tool to verify the fundamental properties of a software system, including safety, liveness, and correlation using an on-the-fly technique.
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). 10241.
https://digital.car.chula.ac.th/chulaetd/10241