Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Railway network modeling using timed coloured petri nets
Year (A.D.)
2018
Document Type
Thesis
First 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.1258
Abstract
การทวนสอบเชิงรูปนัยสามารถนำไปใช้เป็นทางเลือกในการทวนสอบแบบจำลองต้นแบบที่ออกแบบให้ทราบถึงข้อผิดพลาดหรือคุณลักษณะด้านความปลอดภัย แต่อย่างไรก็ตาม การออกแบบแบบจำลองเครือข่ายทางรถไฟขนาดใหญ่ที่มีความซับซ้อนค่อนข้างมากอาจเกิดข้อผิดพลาดขึ้นได้ง่าย วิทยานิพนธ์นี้จึงได้นำเสนอทางเลือกในการสร้างแบบจำลองเครือข่ายทางรถไฟโดยใช้มอดูลที่ถูกสร้างขึ้นจากแบบจำลองไทมด์คัลเลอร์เพทริเน็ตซึ่งเป็นแบบจำลองเชิงรูปนัยแทนการสร้างแบบจำลองไทมด์คัลเลอร์เพทริเน็ตแบบทั่วไป โดยวิทยานิพนธ์ได้นำเสนอมอดูลมาตรฐานที่แทนส่วนประกอบในเครือข่ายทางรถไฟ คือ สถานีรถไฟ และ รางรถไฟ รองรับประเภทรถไฟโดยสาร 3 ประเภทและการควบคุมการเดินรถไฟโดยใช้ตารางเวลารถไฟที่สามารถกำหนดได้ พร้อมทั้งนำเสนอกฎและเงื่อนไขในการต่อประสานมอดูลเหล่านั้นเพื่อประกอบกันเป็นเครือข่ายทางรถไฟขนาดใหญ่ได้ โดยมีเครื่องมือที่ถูกพัฒนาในวิทยานิพนธ์ช่วยเหลือผู้ใช้ในการสร้างและแปลงเครือข่ายทางรถไฟที่ถูกออกแบบไปเป็นไทมด์คัลเลอร์เพทริเน็ต ผลลัพธ์การจำลองแสดงผลผ่านโปรแกรมเครื่องมือ ซีพีเอ็น เพื่อตรวจหาความถูกต้อง และความปลอดภัยของแบบจำลองเครือข่ายทางรถไฟและตารางรถไฟที่นำเข้ามาตรวจสอบ โดยยกตัวอย่างกรณีศึกษาสำหรับเครือข่ายทางรถไฟจำนวน 8 สถานี พร้อมทำการจำลองเหตุการณ์ความล่าช้าที่เกิดขึ้นที่เครือข่ายทางรถไฟ เพื่อตรวจสอบผลกระทบที่เกิดขึ้น
Other Abstract (Other language abstract of ETD)
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.
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). 3389.
https://digital.car.chula.ac.th/chulaetd/3389