Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/74198
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorอาทิตย์ ทองทักษ์-
dc.contributor.advisorวิวัฒน์ วัฒนาวุฒิ-
dc.contributor.authorอรสุธี ชัยชมภู-
dc.contributor.otherจุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์-
dc.date.accessioned2021-06-28T07:59:27Z-
dc.date.available2021-06-28T07:59:27Z-
dc.date.issued2561-
dc.identifier.urihttp://cuir.car.chula.ac.th/handle/123456789/74198-
dc.descriptionวิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2561en_US
dc.description.abstractวิทยานิพนธ์นี้เสนอวิธีการแปลงไทม์เพทริเน็ตเป็นโพรเมลา เพื่อตรวจสอบคุณสมบัติ พฤติกรรมของไทม์เพทริเนตที่เป็นระบบเวลา โดยคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิงคุณภาพ และคุณสมบัติเชิงปริมาณ ประการแรกการสร้างกฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา นำส่วนประกอบของไทม์ เพทริเน็ต ตัวแปรเวลา พฤติกรรมของเวลา พฤติกรรมการเคลื่อนที่โทเค็น และโครงสร้างเนต มาสร้างกฎสี่กฎ ได้แก่ กฎกำหนดชื่อตัวแปรโพรเมลา กฎกำหนดการเปลี่ยนแปลงเวลา กฎการ เคลื่อนที่โทเค็น และกฎโครงสร้างเน็ต ตามลำดับ เมื่อได้กฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา แล้ว จะได้โพราเมลา 4 ส่วน จากนั้นรวมโพรเมลาทั้งหมดจึงได้โพรเมลาของไทม์เพทริ เน็ต ประการที่สองเครื่องมือสนับสนุนการแปลงไทม์เพทริเน็ตเป็นโพรเมลานั้น เนื่องจากไทม์เพทริเน็ตเป็นสัญลักษณ์เชิงรูปภาพ ดังนั้นเปลี่ยนสัญลักษณ์เชิงรูปภาพเป็นข้อมูลตัวอักษรที่เรียกว่าพี เอ็นเอ็มแอล แต่พีเอ็นเอ็มแอลมาตรฐานไม่รองกับไทม์เพทริเน็ต ฉะนั้นวิทยานิพนธ์นี้เสนอพี เอ็นเอ็มสำหรับไทม์เพทริเน็ตด้วย เพื่อทำให้พีเอ็นเอ็มแอลเป็นข้อมูลนำเข้าของเครื่องมือสนับสนุน การแปลงไทม์เพทริเน็ตเป็นโพรเมลา เมื่อนำข้อมูลนำเข้าพีเอ็นเอ็มแอลเข้าเครื่องมือสนับสนุนการ แปลงแล้วจะได้โพรเมลาของไทม์เพทริเน็ตมา ประการที่สามคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิง คุณภาพและคุณสมบัติเชิงปริมาณ โดยการตรวจสอบนำโพรเมลาของไทม์เพทริเน็ตและแอลทีแอล ไปตรวจสอบด้วยเครื่องมือสปิน ได้ผลลัพธ์การตรวจสอบที่ผลลัพธ์การตรวจสอบที่ผ่านและผลลัพธ์ การตรวจสอบที่ไม่ผ่านอันเป็นไปตามผลลัพธ์ที่คาดหวังen_US
dc.description.abstractalternativeThis 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.en_US
dc.language.isothen_US
dc.publisherจุฬาลงกรณ์มหาวิทยาลัยen_US
dc.relation.urihttp://doi.org/10.58837/CHULA.THE.2018.1276-
dc.rightsจุฬาลงกรณ์มหาวิทยาลัยen_US
dc.subjectทฤษฎีกราฟ-
dc.subjectแบบจำลองทางคณิตศาสตร์-
dc.subjectGraph theory-
dc.subjectMathematical models-
dc.subjectPetri nets-
dc.titleการแปลงไทม์เพทริเน็ตเป็นโพรเมลาen_US
dc.title.alternativeTransformation of time petri net into promelaen_US
dc.typeThesisen_US
dc.degree.nameวิทยาศาสตรมหาบัณฑิตen_US
dc.degree.levelปริญญาโทen_US
dc.degree.disciplineวิศวกรรมซอฟต์แวร์en_US
dc.degree.grantorจุฬาลงกรณ์มหาวิทยาลัยen_US
dc.email.advisorArthit.T@Chula.ac.th-
dc.email.advisorWiwat.V@Chula.ac.th,wiwatv@gmail.com,wiwat@chula.ac.th-
dc.identifier.DOI10.58837/CHULA.THE.2018.1276-
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.