Abstract:
งานวิทยานิพนธ์นี้เสนอแบบจำลองเชิงรูปนัยด้วยภาษาโปรเมลา เพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยเครื่องตรวจสอบแบบจำลองสปิน แบบจำลองเชิงรูปนัยที่เป็นผลลัพธ์ประกอบด้วย 5 แบบจำลองย่อย คือ แบบจำลองย่อยสัญญาณนาฬิกา แบบจำลองย่อยภารกิจ แบบจำลองย่อยภารกิจไม่อิสระ แบบจำลองย่อยการจัดกำหนดรายการเวลา และแบบจำลองย่อยเครื่องประมวลผลเอมทีแอล ทั้งนี้เพื่อให้สามารถแสดงขีดความสามารถของระบบเวลาจริงของระบบยูเอวีด้วยเช่นกัน แบบจำลองเชิงรูปนัยผลลัพธ์นี้ไม่เพียงแต่สามารถใช้เพื่อการทวนสอบการจัดกำหนดรายการเวลาการทำงานที่สอดคล้องตามเงื่อนไขของระบบเวลาจริงได้เท่านั้น แต่ยังรองรับภารกิจแบบจวบกันและรวมถึงภารกิจที่มีการประสานเวลาด้วยระบบนับเวลาภายในแบบจำลอง งานวิทยานิพนธ์นี้ยังเสนอวิธีการแปลสัญลักษณ์ตัวดำเนินการเชิงปริมาณพื้นฐานของภาษาเอมทีแอลมาเป็นสูตรภาษาแอลทีแอลเพื่อการทวนสอบระบบเวลาจริงด้วยเครื่องตรวจแบบจำลองสปินได้อย่างอัตโนมัติ
