Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transformation of metric temporal logic into linear temporal logic for promela
Year (A.D.)
2020
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.2020.1144
Abstract
การทวนสอบสำหรับระบบเรียลไทม์เป็นสิ่งสำคัญและหลีกเลี่ยงไม่ได้ โดยปกติแล้วระบบเรียลไทม์จะอยู่ในรูปแบบที่เป็นรูปแบบทางการและถูกตรวจสอบเพื่อให้สามารถรองรับคุณลักษณะที่สำคัญ ๆ ได้ แบบจำลองที่อยู่ในรูปแบบที่เป็นทางการนี้สามารถตรวจสอบคุณลักษณะที่สนใจด้วยใช้การตรวจสอบแบบจำลอง อย่างไรก็ตาม การตรวจสอบคุณลักษณะของแบบจำลองดังกล่าว ที่ได้ประสิทธิภาพสามารถเขียนแทนให้อยู่ในรูปแบบของตรรกเชิงเวลาแบบเมตริก หรือเอ็มทีแอล ซึ่งสามารถระบุช่วงเวลาที่สนใจได้ วิทยานิพนธ์ฉบับนี้ได้นำเสนอทางเลือกหนึ่งสำหรับการแปลงสมการในรูปบบแอลทีแอลไปเป็นสมการในรูปแบบของตรรกศาสตร์เชิงเส้น หรือแอลทีแอล ที่ทำงานร่วมกันกับภาษาโพรเมลา จากคุณลักษณะของเอ็มทีแอลที่ประกอบไปด้วย ตัวดำเนินการแบบตลอดไป ตัวดำเนินการแบบในที่สุด ตัวดำเนินการแบบถัดไป ตัวดำเนินการจนกระทั่งแบบเข้ม และตัวดำเนินการจนกระทั่งแบบอ่อน จากคุณะลักษณะทั้งหมดที่กล่าวมานั้นเป็นคุณลักษณะที่ได้นำมาศึกษาในวิทยานิพนธ์ฉบับนี้ กรณีศึกษาแบบจำลองระบบการบรรจุในแจ้งยอดหนี้บัตรเครดิตที่อยู่ในรูปแบบของไทม์แพททริเนทและถูกเขียนด้วยภาษาโพรเมลาซึ่งทำงานด้วยระบบสัญญาณนาฬิกาหลักและนาฬิกาย่อยเพื่อรองรับการทำงานกับเงื่อนไขด้านเวลาของกระบวนการในกรณีศึกษา การแปลงสมการในรูปแบบของเอ็มทีแอลพร้อมด้วยเงื่อนไขของเวลาไปเป็นสมการในรูปแบบของแอลทีแอลแสดงให้เห็นว่าการทวนสอบแบบจำลองกรณีศึกษาทำงานได้อย่างถูกต้องโดยทวนสอบแบบจำลองดังกล่าวด้วยเครื่องมือสปิน
Other Abstract (Other language abstract of ETD)
Formal verification for the real-time systems is crucial and inevitable. Typically, a real-time system is formalized and verified to ensure the critical properties. The formal model and its desirable properties may be checked using model checker. However, the target properties may be efficiently written in metric temporal logic (MTL) providing the time duration checking. In this thesis, we propose an alternative to transform the given MTL formula into the conventional linear temporal logic (LTL) formula in order to work along with Promela code. The following MTL operators - operators of Always, Eventually, Next, Strong Until, and Weak Until, are focused in this thesis. A case study of credit card billing system model is formalized into Timed Petri net and translated into Promela code with the multi-level clock system – Global clock and local clocks, to cope with the time constraints among the activities in the case study. The transformation of the MTL formula with time constraints into the corresponding LTL formula is demonstrated. The formal verification of the case study is correctly conducted using SPIN tool.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
กะวิเศษ, จุฑามาศ, "การแปลงตรรกเชิงเวลาแบบเมตริกไปเป็นตรรกเชิงเวลาเชิงเส้นสำหรับโพรเมลา" (2020). Chulalongkorn University Theses and Dissertations (Chula ETD). 3802.
https://digital.car.chula.ac.th/chulaetd/3802