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.

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.