การแปลงตรรกเชิงเวลาแบบเมตริกไปเป็นตรรกเชิงเวลาเชิงเส้นสำหรับโพรเมลา

Abstract

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