Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/74198
Title: การแปลงไทม์เพทริเน็ตเป็นโพรเมลา
Other Titles: Transformation of time petri net into promela
Authors: อรสุธี ชัยชมภู
Advisors: อาทิตย์ ทองทักษ์
วิวัฒน์ วัฒนาวุฒิ
Other author: จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
Advisor's Email: Arthit.T@Chula.ac.th
Wiwat.V@Chula.ac.th,wiwatv@gmail.com,wiwat@chula.ac.th
Subjects: ทฤษฎีกราฟ
แบบจำลองทางคณิตศาสตร์
Graph theory
Mathematical models
Petri nets
Issue Date: 2561
Publisher: จุฬาลงกรณ์มหาวิทยาลัย
Abstract: วิทยานิพนธ์นี้เสนอวิธีการแปลงไทม์เพทริเน็ตเป็นโพรเมลา เพื่อตรวจสอบคุณสมบัติ พฤติกรรมของไทม์เพทริเนตที่เป็นระบบเวลา โดยคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิงคุณภาพ และคุณสมบัติเชิงปริมาณ ประการแรกการสร้างกฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา นำส่วนประกอบของไทม์ เพทริเน็ต ตัวแปรเวลา พฤติกรรมของเวลา พฤติกรรมการเคลื่อนที่โทเค็น และโครงสร้างเนต มาสร้างกฎสี่กฎ ได้แก่ กฎกำหนดชื่อตัวแปรโพรเมลา กฎกำหนดการเปลี่ยนแปลงเวลา กฎการ เคลื่อนที่โทเค็น และกฎโครงสร้างเน็ต ตามลำดับ เมื่อได้กฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา แล้ว จะได้โพราเมลา 4 ส่วน จากนั้นรวมโพรเมลาทั้งหมดจึงได้โพรเมลาของไทม์เพทริ เน็ต ประการที่สองเครื่องมือสนับสนุนการแปลงไทม์เพทริเน็ตเป็นโพรเมลานั้น เนื่องจากไทม์เพทริเน็ตเป็นสัญลักษณ์เชิงรูปภาพ ดังนั้นเปลี่ยนสัญลักษณ์เชิงรูปภาพเป็นข้อมูลตัวอักษรที่เรียกว่าพี เอ็นเอ็มแอล แต่พีเอ็นเอ็มแอลมาตรฐานไม่รองกับไทม์เพทริเน็ต ฉะนั้นวิทยานิพนธ์นี้เสนอพี เอ็นเอ็มสำหรับไทม์เพทริเน็ตด้วย เพื่อทำให้พีเอ็นเอ็มแอลเป็นข้อมูลนำเข้าของเครื่องมือสนับสนุน การแปลงไทม์เพทริเน็ตเป็นโพรเมลา เมื่อนำข้อมูลนำเข้าพีเอ็นเอ็มแอลเข้าเครื่องมือสนับสนุนการ แปลงแล้วจะได้โพรเมลาของไทม์เพทริเน็ตมา ประการที่สามคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิง คุณภาพและคุณสมบัติเชิงปริมาณ โดยการตรวจสอบนำโพรเมลาของไทม์เพทริเน็ตและแอลทีแอล ไปตรวจสอบด้วยเครื่องมือสปิน ได้ผลลัพธ์การตรวจสอบที่ผลลัพธ์การตรวจสอบที่ผ่านและผลลัพธ์ การตรวจสอบที่ไม่ผ่านอันเป็นไปตามผลลัพธ์ที่คาดหวัง
Other Abstract: This thesis proposes a method transformation of Time Petri net into Promela. To verify Time Petri net behavioral which is time system. Property verified are qualitative and quantitative. Firstly, Rule creation of transformation of Time Petri net into Promela. Take the component of Time Petri net, time behavior, token dynamic behavior, and net structure. Which are used create four rules respectively: rule of declare Promela variable, rule of time behavior, rule of token dynamic behavior, and rule of net structure. After rules creation, there are 4 Promela parts. Then assemble all parts which is Promela of Time Petri net. Secondly, the tool which support transformation of Time Petri net into Promela. Because Time Petri net is graphic symbol Therefore, changing the graphic symbol is character data called PNML. But the standard PMNL is not match to Time Petri net. So, this thesis proposes PNML for Time Petri net as well. For import PNML data into the tool which support transformation of Time Petri net into Promela, when importing PNML input data into the tool, then Promela of Time Petri net created. Thirdly, Property verified are qualitative and quantitative. Verification Promela of Time Petri net with LTL using SPIN, verification results are both passed result and failed result, which satisfied expected results.
Description: วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2561
Degree Name: วิทยาศาสตรมหาบัณฑิต
Degree Level: ปริญญาโท
Degree Discipline: วิศวกรรมซอฟต์แวร์
URI: http://cuir.car.chula.ac.th/handle/123456789/74198
URI: http://doi.org/10.58837/CHULA.THE.2018.1276
metadata.dc.identifier.DOI: 10.58837/CHULA.THE.2018.1276
Type: Thesis
Appears in Collections:Eng - Theses

Files in This Item:
File Description SizeFormat 
En_5870985821_Onsuthee Ch.pdf2.7 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.