Please use this identifier to cite or link to this item: http://cuir.car.chula.ac.th/handle/123456789/61595
Title: Railway Network Modeling Using Timed Coloured Petri Nets
การสร้างแบบจำลองเครือข่ายทางรถไฟด้วยไทมด์คัลเลอร์เพทริเน็ต
Advisors: Wiwat Vatanawood
วิวัฒน์ วัฒนาวุฒิ
Other author: Chulalongkorn University. Faculty of Engineering
Subjects: การทวนสอบเชิงรูปนัย
เครือข่ายทางรถไฟ
รถไฟ
คัลเลอร์เพทริเน็ต
ไทมด์คัลเลอร์เพทริเน็ต
Formal Verification
Petri Nets
Coloured Petri Nets
Timed Coloured Petri Nets
Railway Network
Railway
Modeling
Issue Date: 2561
Publisher: Chulalongkorn University
Abstract:  Formal verification is likely an alternative to check safety property of the system model. However, to design an abstract model of huge railway network manually may cause errors because of its complexity. This thesis proposes an alternative to generate a formal railway network model from the module of Timed Coloured Petri Nets. Instead of constructing the formal model of a railway network model from scratch using CPN Tools, we provide a set of predefined modules of the high-level railway network components, including a train station module, a rail module, etc. A set of mapping rules is provided to generate the high-level railway network in terms of modules, into Timed Coloured Petri Nets automatically by the developed tool.   The resulting formal model is verified using CPN Tools to ensure the correctness, safety, and liveness of the formal railway network model.
 การทวนสอบเชิงรูปนัยสามารถนำไปใช้เป็นทางเลือกในการทวนสอบแบบจำลองต้นแบบที่ออกแบบให้ทราบถึงข้อผิดพลาดหรือคุณลักษณะด้านความปลอดภัย แต่อย่างไรก็ตาม การออกแบบแบบจำลองเครือข่ายทางรถไฟขนาดใหญ่ที่มีความซับซ้อนค่อนข้างมากอาจเกิดข้อผิดพลาดขึ้นได้ง่าย  วิทยานิพนธ์นี้จึงได้นำเสนอทางเลือกในการสร้างแบบจำลองเครือข่ายทางรถไฟโดยใช้มอดูลที่ถูกสร้างขึ้นจากแบบจำลองไทมด์คัลเลอร์เพทริเน็ตซึ่งเป็นแบบจำลองเชิงรูปนัยแทนการสร้างแบบจำลองไทมด์คัลเลอร์เพทริเน็ตแบบทั่วไป โดยวิทยานิพนธ์ได้นำเสนอมอดูลมาตรฐานที่แทนส่วนประกอบในเครือข่ายทางรถไฟ คือ สถานีรถไฟ และ รางรถไฟ รองรับประเภทรถไฟโดยสาร 3 ประเภทและการควบคุมการเดินรถไฟโดยใช้ตารางเวลารถไฟที่สามารถกำหนดได้  พร้อมทั้งนำเสนอกฎและเงื่อนไขในการต่อประสานมอดูลเหล่านั้นเพื่อประกอบกันเป็นเครือข่ายทางรถไฟขนาดใหญ่ได้ โดยมีเครื่องมือที่ถูกพัฒนาในวิทยานิพนธ์ช่วยเหลือผู้ใช้ในการสร้างและแปลงเครือข่ายทางรถไฟที่ถูกออกแบบไปเป็นไทมด์คัลเลอร์เพทริเน็ต  ผลลัพธ์การจำลองแสดงผลผ่านโปรแกรมเครื่องมือ ซีพีเอ็น เพื่อตรวจหาความถูกต้อง และความปลอดภัยของแบบจำลองเครือข่ายทางรถไฟและตารางรถไฟที่นำเข้ามาตรวจสอบ โดยยกตัวอย่างกรณีศึกษาสำหรับเครือข่ายทางรถไฟจำนวน 8 สถานี พร้อมทำการจำลองเหตุการณ์ความล่าช้าที่เกิดขึ้นที่เครือข่ายทางรถไฟ เพื่อตรวจสอบผลกระทบที่เกิดขึ้น
Description: Master of Science (M.Sc.)
วิทยาศาสตรมหาบัณฑิต (วท.ม.)
URI: http://cuir.car.chula.ac.th/handle/123456789/61595
Type: Thesis
วิทยานิพนธ์
Appears in Collections:FACULTY OF ENGINEERING

Files in This Item:
File Description SizeFormat 
5971013021.pdf5.47 MBAdobe PDFView/Open


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