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

จุฑามาศ กะวิเศษ

dc.contributor.advisor	วิวัฒน์ วัฒนาวุฒิ
dc.contributor.author	จุฑามาศ กะวิเศษ
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
dc.date.accessioned	2021-09-22T23:25:45Z
dc.date.available	2021-09-22T23:25:45Z
dc.date.issued	2563
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/77084
dc.description	วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2563
dc.description.abstract	การทวนสอบสำหรับระบบเรียลไทม์เป็นสิ่งสำคัญและหลีกเลี่ยงไม่ได้ โดยปกติแล้วระบบเรียลไทม์จะอยู่ในรูปแบบที่เป็นรูปแบบทางการและถูกตรวจสอบเพื่อให้สามารถรองรับคุณลักษณะที่สำคัญ ๆ ได้ แบบจำลองที่อยู่ในรูปแบบที่เป็นทางการนี้สามารถตรวจสอบคุณลักษณะที่สนใจด้วยใช้การตรวจสอบแบบจำลอง อย่างไรก็ตาม การตรวจสอบคุณลักษณะของแบบจำลองดังกล่าว ที่ได้ประสิทธิภาพสามารถเขียนแทนให้อยู่ในรูปแบบของตรรกเชิงเวลาแบบเมตริก หรือเอ็มทีแอล ซึ่งสามารถระบุช่วงเวลาที่สนใจได้ วิทยานิพนธ์ฉบับนี้ได้นำเสนอทางเลือกหนึ่งสำหรับการแปลงสมการในรูปบบแอลทีแอลไปเป็นสมการในรูปแบบของตรรกศาสตร์เชิงเส้น หรือแอลทีแอล ที่ทำงานร่วมกันกับภาษาโพรเมลา จากคุณลักษณะของเอ็มทีแอลที่ประกอบไปด้วย ตัวดำเนินการแบบตลอดไป ตัวดำเนินการแบบในที่สุด ตัวดำเนินการแบบถัดไป ตัวดำเนินการจนกระทั่งแบบเข้ม และตัวดำเนินการจนกระทั่งแบบอ่อน จากคุณะลักษณะทั้งหมดที่กล่าวมานั้นเป็นคุณลักษณะที่ได้นำมาศึกษาในวิทยานิพนธ์ฉบับนี้ กรณีศึกษาแบบจำลองระบบการบรรจุในแจ้งยอดหนี้บัตรเครดิตที่อยู่ในรูปแบบของไทม์แพททริเนทและถูกเขียนด้วยภาษาโพรเมลาซึ่งทำงานด้วยระบบสัญญาณนาฬิกาหลักและนาฬิกาย่อยเพื่อรองรับการทำงานกับเงื่อนไขด้านเวลาของกระบวนการในกรณีศึกษา การแปลงสมการในรูปแบบของเอ็มทีแอลพร้อมด้วยเงื่อนไขของเวลาไปเป็นสมการในรูปแบบของแอลทีแอลแสดงให้เห็นว่าการทวนสอบแบบจำลองกรณีศึกษาทำงานได้อย่างถูกต้องโดยทวนสอบแบบจำลองดังกล่าวด้วยเครื่องมือสปิน
dc.description.abstractalternative	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.
dc.language.iso	th
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย
dc.relation.uri	http://doi.org/10.58837/CHULA.THE.2020.1144
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย
dc.subject.classification	Engineering
dc.title	การแปลงตรรกเชิงเวลาแบบเมตริกไปเป็นตรรกเชิงเวลาเชิงเส้นสำหรับโพรเมลา
dc.title.alternative	Transformation of metric temporal logic into linear temporal logic for promela
dc.type	Thesis
dc.degree.name	วิทยาศาสตรมหาบัณฑิต
dc.degree.level	ปริญญาโท
dc.degree.discipline	วิศวกรรมซอฟต์แวร์
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย
dc.identifier.DOI	10.58837/CHULA.THE.2020.1144