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

Abstract

กระบวนการทวนสอบเชิงรูปนัยเป็นสิ่งที่สำคัญในการตรวจสอบความปลอดภัย ความดำเนินชีวิตและความสัมพันธ์ของระบบซอฟต์แวร์ตั้งแต่เริ่มต้นออกแบบซอฟต์แวร์ ซึ่งสามารถช่วยให้ลดความพยายามในการพัฒนาอย่างเห็นได้ชัด โมเดลเช็กกิงเป็นวิธีการเชิงรูปนัยอย่างหนึ่งที่สามารถทวนสอบระบบซอฟต์แวร์ตามคุณสมบัติเชิงพฤติกรรมที่เขียนเป็นสูตรตรรกศาสตร์เชิงเวลาแบบลำดับหรือเรียกว่าสูตรแอลทีแอล โดยใช้วิธีการสำรวจเส้นทางดำเนินงานที่เป็นไปได้ทั้งหมดอย่างละเอียดถี่ถ้วนในปริภูมิสถานะของระบบซอฟต์แวร์และกำหนดว่าเส้นทางดำเนินงานทั้งหมดของระบบเป็นไปตามคุณสมบัติที่เขียนโดยใช้สูตรแอลทีแอลหรือไม่ อย่างไรก็ตาม ระบบที่มีขนาดใหญ่และมีความซับซ้อนอาจทำให้เกิดการระเบิดของปริภูมิสถานะในการทำโมเดลเช็กกิงได้ ซึ่งมีการเสนอวิธีการลดพื้นที่ของปริภูมิสถานะหลายวิธีและแม้แต่วิธีการของแมชชีนเลิร์นนิงก็ถูกนำมาใช้เพื่อทำนายผลลัพธ์ความพึงพอใจของคุณสมบัติแอลทีแอลของระบบซอฟต์แวร์ เมื่อพิจารณาถึงความสำเร็จในการฝึกอบรมโครงข่ายความจำระยะสั้นแบบยาวหรือแอลเอสทีเอ็มสำหรับการทำนายลำดับข้อมูลอนุกรมเวลาแบบยาว ในวิทยานิพนธ์นี้ ได้เสนอแนวคิดแอลเอสทีเอ็มที่ขยายการจำแนกแบบหลายป้ายและกลยุทธ์การหาขีดแบ่งเพื่อบรรเทาปัญหาการระเบิดของปริภูมิสถานะและสร้างเป็นเครื่องสร้างปริภูมิสถานะสำหรับสร้างเส้นทางดำเนินงานของระบบซอฟต์แวร์ได้ตามที่ต้องการ โดย ได้สร้างเครื่องมือในการทวนสอบคุณสมบัติพื้นฐานของระบบซอฟต์แวร์ ได้แก่ คุณสมบัติด้านความปลอดภัย ด้านความดำเนินชีวิตและด้านความสัมพันธ์ ด้วยเทคนิคออน-เดอะ-ฟลาย