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.

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.