เครื่องสร้างปริภูมิสถานะสำหรับโมเดลเช็กกิงแบบแอลทีแอลโดยใช้แอลเอสทีเอ็มที่มีการจำแนกแบบหลายป้าย

ชลิกา ศักดิ์สุภาวัฒนกุล

dc.contributor.advisor	วิวัฒน์ วัฒนาวุฒิ
dc.contributor.author	ชลิกา ศักดิ์สุภาวัฒนกุล
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
dc.date.accessioned	2024-02-05T10:12:34Z
dc.date.available	2024-02-05T10:12:34Z
dc.date.issued	2566
dc.identifier.uri	https://cuir.car.chula.ac.th/handle/123456789/84319
dc.description	วิทยานิพนธ์ (วศ.ด.)--จุฬาลงกรณ์มหาวิทยาลัย, 2565
dc.description.abstract	กระบวนการทวนสอบเชิงรูปนัยเป็นสิ่งที่สำคัญในการตรวจสอบความปลอดภัย ความดำเนินชีวิตและความสัมพันธ์ของระบบซอฟต์แวร์ตั้งแต่เริ่มต้นออกแบบซอฟต์แวร์ ซึ่งสามารถช่วยให้ลดความพยายามในการพัฒนาอย่างเห็นได้ชัด โมเดลเช็กกิงเป็นวิธีการเชิงรูปนัยอย่างหนึ่งที่สามารถทวนสอบระบบซอฟต์แวร์ตามคุณสมบัติเชิงพฤติกรรมที่เขียนเป็นสูตรตรรกศาสตร์เชิงเวลาแบบลำดับหรือเรียกว่าสูตรแอลทีแอล โดยใช้วิธีการสำรวจเส้นทางดำเนินงานที่เป็นไปได้ทั้งหมดอย่างละเอียดถี่ถ้วนในปริภูมิสถานะของระบบซอฟต์แวร์และกำหนดว่าเส้นทางดำเนินงานทั้งหมดของระบบเป็นไปตามคุณสมบัติที่เขียนโดยใช้สูตรแอลทีแอลหรือไม่ อย่างไรก็ตาม ระบบที่มีขนาดใหญ่และมีความซับซ้อนอาจทำให้เกิดการระเบิดของปริภูมิสถานะในการทำโมเดลเช็กกิงได้ ซึ่งมีการเสนอวิธีการลดพื้นที่ของปริภูมิสถานะหลายวิธีและแม้แต่วิธีการของแมชชีนเลิร์นนิงก็ถูกนำมาใช้เพื่อทำนายผลลัพธ์ความพึงพอใจของคุณสมบัติแอลทีแอลของระบบซอฟต์แวร์ เมื่อพิจารณาถึงความสำเร็จในการฝึกอบรมโครงข่ายความจำระยะสั้นแบบยาวหรือแอลเอสทีเอ็มสำหรับการทำนายลำดับข้อมูลอนุกรมเวลาแบบยาว ในวิทยานิพนธ์นี้ ได้เสนอแนวคิดแอลเอสทีเอ็มที่ขยายการจำแนกแบบหลายป้ายและกลยุทธ์การหาขีดแบ่งเพื่อบรรเทาปัญหาการระเบิดของปริภูมิสถานะและสร้างเป็นเครื่องสร้างปริภูมิสถานะสำหรับสร้างเส้นทางดำเนินงานของระบบซอฟต์แวร์ได้ตามที่ต้องการ โดย ได้สร้างเครื่องมือในการทวนสอบคุณสมบัติพื้นฐานของระบบซอฟต์แวร์ ได้แก่ คุณสมบัติด้านความปลอดภัย ด้านความดำเนินชีวิตและด้านความสัมพันธ์ ด้วยเทคนิคออน-เดอะ-ฟลาย
dc.description.abstractalternative	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.
dc.language.iso	th
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย
dc.subject.classification	Engineering
dc.subject.classification	Engineering
dc.subject.classification	Manufacturing
dc.subject.classification	Computer science
dc.title	เครื่องสร้างปริภูมิสถานะสำหรับโมเดลเช็กกิงแบบแอลทีแอลโดยใช้แอลเอสทีเอ็มที่มีการจำแนกแบบหลายป้าย
dc.title.alternative	State Space Generator for LTL Model Checking using LSTM with Multi-Label Classification
dc.type	Thesis
dc.degree.name	วิศวกรรมศาสตรดุษฎีบัณฑิต
dc.degree.level	ปริญญาเอก
dc.degree.discipline	วิศวกรรมคอมพิวเตอร์
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย