Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transformation of time petri net into promela
Year (A.D.)
2018
Document Type
Thesis
First Advisor
อาทิตย์ ทองทักษ์
Second Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิทยาศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิศวกรรมซอฟต์แวร์
DOI
10.58837/CHULA.THE.2018.1276
Abstract
วิทยานิพนธ์นี้เสนอวิธีการแปลงไทม์เพทริเน็ตเป็นโพรเมลา เพื่อตรวจสอบคุณสมบัติ พฤติกรรมของไทม์เพทริเนตที่เป็นระบบเวลา โดยคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิงคุณภาพ และคุณสมบัติเชิงปริมาณ ประการแรกการสร้างกฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา นำส่วนประกอบของไทม์ เพทริเน็ต ตัวแปรเวลา พฤติกรรมของเวลา พฤติกรรมการเคลื่อนที่โทเค็น และโครงสร้างเนต มาสร้างกฎสี่กฎ ได้แก่ กฎกำหนดชื่อตัวแปรโพรเมลา กฎกำหนดการเปลี่ยนแปลงเวลา กฎการ เคลื่อนที่โทเค็น และกฎโครงสร้างเน็ต ตามลำดับ เมื่อได้กฎการแปลงไทม์เพทริเน็ตเป็นโพรเมลา แล้ว จะได้โพราเมลา 4 ส่วน จากนั้นรวมโพรเมลาทั้งหมดจึงได้โพรเมลาของไทม์เพทริ เน็ต ประการที่สองเครื่องมือสนับสนุนการแปลงไทม์เพทริเน็ตเป็นโพรเมลานั้น เนื่องจากไทม์เพทริเน็ตเป็นสัญลักษณ์เชิงรูปภาพ ดังนั้นเปลี่ยนสัญลักษณ์เชิงรูปภาพเป็นข้อมูลตัวอักษรที่เรียกว่าพี เอ็นเอ็มแอล แต่พีเอ็นเอ็มแอลมาตรฐานไม่รองกับไทม์เพทริเน็ต ฉะนั้นวิทยานิพนธ์นี้เสนอพี เอ็นเอ็มสำหรับไทม์เพทริเน็ตด้วย เพื่อทำให้พีเอ็นเอ็มแอลเป็นข้อมูลนำเข้าของเครื่องมือสนับสนุน การแปลงไทม์เพทริเน็ตเป็นโพรเมลา เมื่อนำข้อมูลนำเข้าพีเอ็นเอ็มแอลเข้าเครื่องมือสนับสนุนการ แปลงแล้วจะได้โพรเมลาของไทม์เพทริเน็ตมา ประการที่สามคุณสมบัติที่ตรวจสอบมีคุณสมบัติเชิง คุณภาพและคุณสมบัติเชิงปริมาณ โดยการตรวจสอบนำโพรเมลาของไทม์เพทริเน็ตและแอลทีแอล ไปตรวจสอบด้วยเครื่องมือสปิน ได้ผลลัพธ์การตรวจสอบที่ผลลัพธ์การตรวจสอบที่ผ่านและผลลัพธ์ การตรวจสอบที่ไม่ผ่านอันเป็นไปตามผลลัพธ์ที่คาดหวัง
Other Abstract (Other language abstract of ETD)
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.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
ชัยชมภู, อรสุธี, "การแปลงไทม์เพทริเน็ตเป็นโพรเมลา" (2018). Chulalongkorn University Theses and Dissertations (Chula ETD). 3407.
https://digital.car.chula.ac.th/chulaetd/3407