Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/74198
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | อาทิตย์ ทองทักษ์ | - |
dc.contributor.advisor | วิวัฒน์ วัฒนาวุฒิ | - |
dc.contributor.author | อรสุธี ชัยชมภู | - |
dc.contributor.other | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ | - |
dc.date.accessioned | 2021-06-28T07:59:27Z | - |
dc.date.available | 2021-06-28T07:59:27Z | - |
dc.date.issued | 2561 | - |
dc.identifier.uri | http://cuir.car.chula.ac.th/handle/123456789/74198 | - |
dc.description | วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2561 | en_US |
dc.description.abstract | วิทยานิพนธ์นี้เสนอวิธีการแปลงไทม์เพทริเน็ตเป็นโพรเมลา เพื่อตรวจสอบคุณสมบัติ พฤติกรรมของไทม์เพทริเนตที่เป็นระบบเวลา โดยคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิงคุณภาพ และคุณสมบัติเชิงปริมาณ ประการแรกการสร้างกฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา นำส่วนประกอบของไทม์ เพทริเน็ต ตัวแปรเวลา พฤติกรรมของเวลา พฤติกรรมการเคลื่อนที่โทเค็น และโครงสร้างเนต มาสร้างกฎสี่กฎ ได้แก่ กฎกำหนดชื่อตัวแปรโพรเมลา กฎกำหนดการเปลี่ยนแปลงเวลา กฎการ เคลื่อนที่โทเค็น และกฎโครงสร้างเน็ต ตามลำดับ เมื่อได้กฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา แล้ว จะได้โพราเมลา 4 ส่วน จากนั้นรวมโพรเมลาทั้งหมดจึงได้โพรเมลาของไทม์เพทริ เน็ต ประการที่สองเครื่องมือสนับสนุนการแปลงไทม์เพทริเน็ตเป็นโพรเมลานั้น เนื่องจากไทม์เพทริเน็ตเป็นสัญลักษณ์เชิงรูปภาพ ดังนั้นเปลี่ยนสัญลักษณ์เชิงรูปภาพเป็นข้อมูลตัวอักษรที่เรียกว่าพี เอ็นเอ็มแอล แต่พีเอ็นเอ็มแอลมาตรฐานไม่รองกับไทม์เพทริเน็ต ฉะนั้นวิทยานิพนธ์นี้เสนอพี เอ็นเอ็มสำหรับไทม์เพทริเน็ตด้วย เพื่อทำให้พีเอ็นเอ็มแอลเป็นข้อมูลนำเข้าของเครื่องมือสนับสนุน การแปลงไทม์เพทริเน็ตเป็นโพรเมลา เมื่อนำข้อมูลนำเข้าพีเอ็นเอ็มแอลเข้าเครื่องมือสนับสนุนการ แปลงแล้วจะได้โพรเมลาของไทม์เพทริเน็ตมา ประการที่สามคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิง คุณภาพและคุณสมบัติเชิงปริมาณ โดยการตรวจสอบนำโพรเมลาของไทม์เพทริเน็ตและแอลทีแอล ไปตรวจสอบด้วยเครื่องมือสปิน ได้ผลลัพธ์การตรวจสอบที่ผลลัพธ์การตรวจสอบที่ผ่านและผลลัพธ์ การตรวจสอบที่ไม่ผ่านอันเป็นไปตามผลลัพธ์ที่คาดหวัง | en_US |
dc.description.abstractalternative | 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. | en_US |
dc.language.iso | th | en_US |
dc.publisher | จุฬาลงกรณ์มหาวิทยาลัย | en_US |
dc.relation.uri | http://doi.org/10.58837/CHULA.THE.2018.1276 | - |
dc.rights | จุฬาลงกรณ์มหาวิทยาลัย | en_US |
dc.subject | ทฤษฎีกราฟ | - |
dc.subject | แบบจำลองทางคณิตศาสตร์ | - |
dc.subject | Graph theory | - |
dc.subject | Mathematical models | - |
dc.subject | Petri nets | - |
dc.title | การแปลงไทม์เพทริเน็ตเป็นโพรเมลา | en_US |
dc.title.alternative | Transformation of time petri net into promela | en_US |
dc.type | Thesis | en_US |
dc.degree.name | วิทยาศาสตรมหาบัณฑิต | en_US |
dc.degree.level | ปริญญาโท | en_US |
dc.degree.discipline | วิศวกรรมซอฟต์แวร์ | en_US |
dc.degree.grantor | จุฬาลงกรณ์มหาวิทยาลัย | en_US |
dc.email.advisor | Arthit.T@Chula.ac.th | - |
dc.email.advisor | Wiwat.V@Chula.ac.th,wiwatv@gmail.com,wiwat@chula.ac.th | - |
dc.identifier.DOI | 10.58837/CHULA.THE.2018.1276 | - |
Appears in Collections: | Eng - Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
En_5870985821_Onsuthee Ch.pdf | 2.7 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.