Please use this identifier to cite or link to this item: http://hdl.handle.net/11527/16503
Title: Designing, Verification And Validation Of Railway Signaling Systems Using Coloured Petri Nets
Other Titles: Demiryolu Sinyalizasyon Sistemleri İçin Renkli Petri Ağlarını Kullanarak Tasarım, Doğrulama Ve Onaylama
Authors: Söylemez, Mehmet Turan
Elhayek, Ali
10135278
Kontrol ve Otomasyon Mühendisliği
Control and Computer Engineering
Keywords: Demiryolu Sistemleri
Biçimsel Yöntem Yazılım
dallanan Zaman Tabanı
renkli Petri Ağları
Railways Systems
Formal Methods
Colored Petri Nets
Computational Tree Logic
Issue Date: 2016
Publisher: Fen Bilimleri Enstitüsü
Institute of Science and Technology
Abstract: Sadece Amerika Birleşik Devletleri'nde hafta içi her gün 7 milyondan daha fazla kişi ulaşımda demiryollarını kullanmaktadır. Aynı zamanda demiryolu, güvenilir yük taşımacılığı yolu olarak yaygın bir şekilde kullanılmaktadır. Genel olarak demiryolu çok önemli bir ulaşım yöntemi olarak düşünülebilir, bu önem ise onun nispeten daha ucuz ve çevre dostu olmasından kaynaklanmaktadır. Bu da birçok ülkede demiryollarının ana ulaşım sistemi olarak kullanılmasına olanak sağlamaktadır. Demiryolu sistemlerinde esas olarak insan hataları ve sistem arızaları gibi çeşitli sebeplerden dolayı kazalar meydana gelmektedir. Çok sayıda insanın demiryollarını kullanması demiryollarının güvenliğini de bu ölçüde önemli kılmaktadır. Bu durum, bazı hükumetlerin demiryolları sistemlerinin operasyonlarında düzenlemek için standartlar koyarak müdahale etmelerine sebep olmuştur. Demiryolu sistemlerinde faaliyette bulunan trenler ve demiryolu sistemlerinin diğer bileşenlerinin güvenliğini sağlanması sinyalizasyon sistemlerinin sorumluluğundadır. Sinyalizasyon kazalardan kaçınmak amacıyla, trafik için optimum kontrol sağlamaktadır. Biçimsel yöntem yazılım geliştirmede çok önemli bir role sahiptir. Biçimsel yöntem ayrık matematik tekniklerinde ve yazılım ve donanım geliştirme sürecinde kullanılan yöntemlerdir. Matematiksel notasyonlar ise yazılım ve donanım sistemlerinin tasarım ve gerçeklemesinde kullanılmaktadır. Biçimsel yöntemleri kullanmanın temel amacı, bir tasarımın tüm durum uzay modelini sembolik olarak inceleyerek önemli özellikler ve tasarım hataları nedeniyle oluşabilecek riskli sonuçları azaltmaktır. Biçimsel yöntemler oluşturulan yazılımda hassas kayıt sunmaya yardımcı olmaktadır bu nedenle gerçekleme ve doğrulama süreçlerinde yaygın olarak kullanılmaktadır. Biçimsel yöntem kullanarak yazılım geliştirmek için, biçimsel dil ve semantik kullanılarak davranış ve özellikleri tanımlamak için Kurallı Belirtim kullanılmaktır. Biçimsel Dil kesin bir şekilde Kurallar tanımlamak için kullanılmaktadır. Biçimsel dil, dilbilgisi kurallarını tanımlamaktadır ve genel algoritmaların kullanılmasını haklı çıkarmaktadır. Semantik her ifadeye kesin bir matematiksel anlam sağlamaktadır. Bu öğeler bir araya getirildiğinde ise geliştiricilerin beklenen özellikleri belirtmelerine ve daha sonra biçimsel olarak doğrulamalarına olanak tanıyan sistem için bir biçimsel model sağlayacaktır. Biçimsel diller ya model tabanlı (Soyut Durum Makineleri, Küme ve sınıf teorisi, otomat tabanlı modelleme ve Gerçek zamanlı sistemler için modelleme dilleri gibi) ya da cebirsel tabanlı olabilmektedir. Petri ağları bir biçimsel yöntemdir. Petri ağı olayları tanımlanmış kurallara dayalı olarak işleyen ve geçişe izin veren koşulları gösterebilen bir cihazdır. Petri ağları Ayrık Olaylı Sistemlerin modellerinde kullanılması ve grafiklerin basit ve karmaşık sistemlerin yapısal bilgilerini tasvir etmesi gibi birçok avantaja sahiptir. Renkli Petri ağları üst düzey Petri ağları grafiksel dildir. Bu normal Petri ağlarına dayanamaktadır ancak jetonlara ve onlarla birlikte çalışan ifadeleri kullanan yerlere renkler eklenmiştir. Model sınama, sistemin sonlu durum modelini ve biçimsel özelliklerini veren bir otomatik tekniktir. Model sınama bu özelliğin o modeldeki belirli durum için tutulup tutulmadığını sistematik olarak kontrol etmektedir.. Model sınama farklı alalarda kullanılabilen genel bir gerçekleme yaklaşımı olarak düşünülmektedir. Bunun yanı sıra model sınama özellikler için kısmi gerçekleme yapabilmektedir, bu da geliştiricinin önemli olanlara odaklanmasını sağlamaktadır. Model sınama diğer gerçekleme yöntemlerine nazaran daha hızlı olduğu düşünülmektedir. Dallanan zaman tabanı (Computational Tree Logic) dallanan zaman ağacıdır ki burada senaryolar, farklı senaryoların uygulanabildiği grafik formdaki hiyearşik yapıyla sembolize edilebilmektedir. Dallanan zaman tabanı* Renkli Petri ağının durum uzayı tarafından gösterilen modellerinin durum ve geçiş özelliklerini ifade etmek için kullanılmaktadır. İkinci bölümün sonunda Renkli Petri Ağları ve Dallanan Zaman Tabanı* ile ilgili tüm kavramları açıkladıkan sonra, Renkli Petri ağlarının nasıl çalıştığını göstermek ve Renkli Petri Ağlı Dallanan Zaman Tabanının gerçekleme ve doğrulama işleminde kullanılabileceğinden emin olmak için basit tren istasyonuna bir örnek verilmiş ve tasarlanmıştır. Üstelik sistemin durum uzay modeli gösterilmiştir ve sistemin durum uzay modeli kullanılarak işaretleme konsepti (concept of marking) açıklanmıştır. Daha karmaşık manevra istasyonu (bu çalışmadaki ana örnek) üçüncü bölümde gösterilmiştir. Manevra istasyonunun bir giriş ve üç çıkışı olmakla birlikte istasyonun hareket kuralları anklaşman tablosuyla tanımlanmış ve bazı kurallar açıklanmıştır. Bu kurallar gerçekleme sürecinde kriter olarak kullanılmıştır. Manevra istasyonuna ait model Renkli Petri Ağları kullanılarak kurulmuştur ve altı trenin manevra istasyonunda tek yönden geçeceği önerilmiştir. Manevra istasyonunda üç çıkış olduğu için üç rota vardır. Olası tüm senaryolar uygulanmıştır. Tüm senaryoların sonunda tüm trenlerin manevra istasyonunun dışında olması gerekmektedir. Simülasyon yürütüldükten sonra tüm trenlerin manevra istasyonunun dışında olduğu simülasyonun sonunda gösterilmiştir. Sistemin doğru bir şekilde çalıştığını doğrulamak için sistemin durum uzay modeli ve sıkı bağlı bileşen grafiği oluşturulmuştur ve sonra sistem durum uzay raporu da oluşturulmuştur. Bundan sonra durum uzay modelinin sonuçlarını ve sıkı bağlı bileşen grafiğini test etmek için bazı sorular yazılmıştır. Sistemi doğrulamak amacıyla üçüncü bölümde belirlenen kurallara göre sorgular da yazılmıştır. Bu sorgular tek tek incelenmiştir ve sistemin belirlenen kurallara uygun olarak çalıştığı gösterilmiştir. Tasarım, gerçekleme ve doğrulama sürecinde kullanılan bilgisayarın özellikleri 4 GB RAM, i5 CPU 2.53 GHz'dir. Kurulan süreç hafızada yaklaşık 62 MB yer tutmuştur ve CPU'nun %29 unu 32 saniye meşgul etmiştir. Renkli Petri Ağları ile sistem modeli oluşturmanın kolay olduğu gösterilmiştir. Gerçekleme ve doğrulama süreçleri de kolaydır çünkü hesaplama açısından pahalı değillerdir. Bu yüzden eğer model oluşturulduysa, sistemin tüm işaretlemelerini (marking) taramak uzun zaman ve çaba gerektirmemektedir. İşaretlemeleri (markings) sınamak sadece Renkli Petri Ağları araçlarını (CPN Tools) kullanarak çok kolay olmamaktadır. Çünkü güncel Petri Ağları araçları (CPN Tools) yeterince geliştirilmemiştir bu yüzden tüm işaretlemelerin( markings) manuel olarak oluşturulması gerekmektedir. Alternatif olarak ise modelin işaretlemelerin oluşturmada karmaşık olan (Graphviz - Graph Visualization Software gibi) bazı araçlar kullanılmaktadır. Bu yöntemin dezavantajı ise sistemin eksiksizliğini garanti etmemesidir. Sadece belirlenen özellikler sınanmaktadır. Dolayısıyla sistemin tüm önemli özelliklerinin belirlenmesi geliştiricinin sorumluluğundadır. Dallanan zaman tabanlı Renkli Petri ağları mevcut petri ağı sistemini doğrulamıştır ancak bu sistem için bir PLC kodu oluşturulmamıştır. Bu yüzden doğrudan Renkli petri ağı modeline dayalı PLC kodu oluşturulabilme olasılığının incelenmesi gerekmektedir.
Every weekday just in United States of America, more than 7 million people use railways in their transportation. In the same time railway is used widely as reliable freight transportation solution. So in general, railway transportation can be considered as a very vital transportation mean, this importance emerges from the fact that railways are relatively cheap and environmental friendly. This enables them to be the main transportation system in many countries. Railways systems are exposed to accidents due to huge variety of reasons like signaling system failures, human errors …etc. As railways are used by a huge number of people, the safety of railways became very important issue. This led some governments to interfere by putting standards in order to organize the operations of railway systems. CENELEC is a safety reference name which states the necessary standards of railway sector and it is composed from the following standards EN 50126, EN 50128 and EN 50129. Based on these standards, Safety Integrity Levels (SILs) were built. Signalling systems are responsible for the operations of railway systems to ensure the safety of trains and their other components. Signalling ensures optimal control for traffic in order to avoid accidents. Formal methods have a very important role in software development. Formal methods are method use the discrete mathematic techniques and tools in software and hardware development process, where the mathematical notations are used in the design and the verification of software and hardware systems. The main purpose of using formal methods is to reduce the risky consequences that can occur due to serious specification and design errors by symbolically examine the entire state space of a design Formal methods help in presenting precise record of the created software that's why it is used widely in verification and validation processes To develop software using formal method, Formal Specifications are used to describe the behavior and properties using formal language and semantics. Formal Language is used to define Rules in a precise manner. Formal language describes the grammar rules and justifies the general algorithms to be used. Semantics provide an accurate mathematical meaning to every statement. These items together will provide a formal model for the system that enables the developers to state the expected properties and then formally verify it Petri net as the models of DES. Petri net graphs depict structural information about the simple and complex systems. Coloured Petri nets are a high-level Petri nets graphical language. It is based on normal PNs, but CTL is a branching time tree; the scenarios can be symbolized by hierarchical structure in a graphical form where different scenarios can be applied. CTL* (or ASK-CTL) is used to express the state and the transition properties of the models interviewed by the state space of the coluored Petri net In this research, a signalling system for a train yard is designed by CPN. The system was verified and validated using model checking which is considered as one of the formal methods. All the processes were performed according to CENELEC to achieve minimum SIL 3.
Description: Tez (Yüksek Lisans) -- İstanbul Teknik Üniversitesi, Fen Bilimleri Enstitüsü, 2016
Thesis (M.Sc.) -- İstanbul Technical University, Institute of Science and Technology, 2016
URI: http://hdl.handle.net/11527/16503
Appears in Collections:Kontrol ve Otomasyon Mühendisliği Lisansüstü Programı - Yüksek Lisans

Files in This Item:
File Description SizeFormat 
10135278.pdf3.02 MBAdobe PDFView/Open


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