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

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

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/77084

Full metadata record

DC Field	Value	Language
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	-
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
5971002121.pdf		2.65 MB	Adobe PDF	View/Open

Show simple item record