Design and rams analysis of railway interlocking systems using formal methods

Abstract

Demiryolu sinyalizasyon sistemleri trenlerin güvenli, planlı ve ekonomik bir şekilde işletilmesini sağlayan sistemlerdir. Geleneksel demiryolu araçları raylar üzerinde çelik ray – çelik tekerlek yöntemi ile yol alırlar. Bu yöntem sayesinde çelik ray ile çelik tekerlek arasındaki sürtünme kuvveti azaltılarak yuvarlanma direnci düşürülmüş olur. Böylelikle trenlerin hareket etmesi için harcanan enerjiden tasarruf edilmiş olur. Fakat bu durum başka bir problemi de beraberinde getirir; Frenleme problemi. Raylar ve tekerlekler arasındaki düşük sürtünme kuvveti fren mesafesinin, makinistlerin görüş mesafesinden daha uzun olmasına neden olur. Bu nedenle trenlerin duruş noktalarından belirli bir mesafe öncesinde fren uygulamaları gerekmektedir. Demiryolu sinyalizasyon sistemlerinin temel amaçlarından biriside fren mesafesini hesaba katarak trenlerin hareket güvenliğini sağlamaktır.Demiryollarında çeşitli amaçlarla çeşitli cihazlar kullanılır. Örneğin makaslar rayların bağlantısını değiştirerek trenlerin bir raydan başka bir raya geçmesi için kullanılır. Trenler gitmesi gereken güzergâhlarda ilerlerken çok sayıda makasın üzerinden geçerler ve tüm bu makasların güzergâha uygun pozisyona ayarlanmış olması gerekir. Sinyalizasyon sistemleri makas gibi demiryolu cihazların güvenlik kriterleri çerçevesinde otomatik olarak kontrol eder ve güvenliliği garanti eder. Sistemde bu gibi saha ekipmanlarının kontrolü ve güvenli pozisyonda kilitlenmesi işlevleri yerine getiren mekanizma `Anklaşman` olarak adlandırılır.Anklaşman sistemleri, trenlerin güvenli hareket edebilmesi için demiryollarında kullanılan saha ekipmanlarının uygun ve güvenli durumda kilitlenmesini sağlayan sinyalizasyon sistemlerinin temel bileşenidir. Bu tez çalışmasında örnek bir demiryolu anklaşman mekanizmasının formal yöntemler ile tasarlanması ve uygulanması amaçlanmıştır. Tasarlanan basit anklaşman sistemi için dizayn kriteri olarak Alman `Ks` sinyal sistemi dikkate alınmıştır. Fakat çalışmayı basitleştirmek amacı ile Ks sisteminin tüm özellikleri kapsanmamıştır. Birinci bölümde genel manada sinyalizasyon sisteminin ve güvenlik kriterlerinin demiryollarındaki önemi istatistiki bilgilerle anlatılmıştır.İkinci bölümde, demiryolu sinyalizasyon sistemlerinin yapısı ve bu sistemlere neden ihtiyaç duyulduğu açıklanmıştır. Daha sonra sinyalizasyon sistemlerinde kullanılan temel bileşenler ve makas, sinyal lambası, aks sayıcı, vs. gibi temel saha ekipmanları açıklanmıştır.Farklı ülkeler farklı sinyalizasyon prensiplerine sahiptir. İkinci bölümün devamında Alman Ks sinyal sisteminde ve Türk sinyal sisteminde kullanılan sinyalizasyon prensipleri tanımlanmıştır. Her iki sistemde kullanılan sinyal lambaları kullanım yerleri ve anlamları ile açıklanmıştır.Üçüncü bölümde anklaşman terimi açıklandıktan sonra demiryollarındaki karşılığı anlatılmıştır. İlk kullanılan mekanik sistemlerinden günümüzde kullanılan bilgisayar tabanlı modern sistemlere kadar kullanılan farklı yapılardaki anklaşman sistemleri üçüncü bölümde işlenmiştir.Sinyalizasyon sistemlerinde oluşabilecek her hangi bir hata, trenlerin raydan çıkması veya başka trenler ile çarpışması gibi ölümcül sonuçlar doğuracak ciddi tren kazalarına sebep olabilir. Bu nedenle sinyalizasyon sistemleri tasarlanırken sistemin çalışması esnasında oluşabilecek tüm arızalar düşünülerek bu gibi arıza durumlarında sistemin güvenli duruma geçmesi sağlanır. Hatada güvenlilik şeklinde tanımlanan bu prensip üçüncü bölümde örneklerle açıklanmıştır.Anklaşman sistemleri tasarlanırken bir takım temel prensipler dikkate alınır. Üçüncü bölümde bu tasarım prensiplerinden bir kısmı, 2 numaralı kaynaktan faydalanılarak açıklanmıştır.Dördüncü bölümde anklaşman sistemlerinin tasarlanmasında kullanılan formal yöntemler açıklanmıştır. Daha sonra yaygın olarak kullanılan iki yöntem `Petri Ağları` ve `Sonlu Durum Makinaları` tartışılmıştır. Sonlu durum makinaları yönteminin tasarım basamaklarını göstermek amacı ile basit bir turnike cihazının modellenmesi örnek olarak verilmiştir. Dördüncü bölümün devamında, tasarlanacak modelleri gerçeklemek ve test etmek için iki farklı PLC programlama yazılımı avantaj ve dezavantajları ile incelenmiştir. Ardından, daha önce verilen basit örnek model her iki programlama yazılımıyla da gerçeklenmiştir. İleriki bölümlerde tasarlanacak modeller için kullanılacak olan SilworX yazılımının neden tercih edildiği aynı bölümün sonunda açıklanmıştır.Beşinci bölümde bir model demiryolu istasyonu tasarlanmıştır. Tasarlanan model istasyon için hat tipleri ve tren tipleri ve tüm işletme karakteristikleri tanımlanmıştır. Daha sonra sinyalizasyon ekipmanlarının konumlandırılması tartışılmıştır.Altıncı bölümde model istasyon için olası tüm tren güzergâhlarını gösteren bir güzergâh tablosu oluşturulmuştur. Bu tablo anklaşman tasarlanan bölgedeki güzergâhların hangi saha ekipmanlarını kullandığı ve bu saha ekipmanlarının durumunun ne olması gerektiğini gösterir.Altıncı bölümün devamında sonlu durum makinaları yöntemi kullanılarak ikinci bölümde açıklanan hat boyu ekipmanlarının modelleri oluşturulmuş ve PLC programlama yazılımı SilworX ile gerçeklenmiştir. Daha sonra aynı yöntemle güzergâh tablosu dikkate alınarak bazı güzergah tayin etme fonksiyonları modellenmiştir. Son olarak tasarlanan modeller ile güzergah tablosundaki ilk güzergah için tayin etme mekanizması oluşturulmuştur. Daha sonra bu mekanizma SilworX yazılımı ile gerçeklenmiş ve test edilmiştir.Bölüm 7'de sistem tasarımında dikkat edilmesi gereken `Güvenilirlik, Emre amadelik, Sürdürülebilirlik ve Güvenlik` kriterleri işlenmiştir. RAMS kriterleri olarak ifade edilen bu kriterlerin hesaplanması ve analizinde yaygın olarak kullanılan iki adet yöntem `Hata Ağacı Yöntemi` ve `Markov Modeli` aynı bölümde açıklanmıştır. Son olarak beşinci bölümde oluşturulan model istasyon için bir Markov modeli tasarlanmış ve bu model ile RAMS analizinde kullanılan denklemler elde edilmiştir. Bu bölümün sonunda RAMS parametreleri elde edilmiştir.Tez çalışmasında ulaşılan sonuçlar son bölümde gösterilmiştir. Ayrıca bu bölümde tasarlanan anklaşman sistemi ve gelecekte yapılabilecekler tartışılmıştır.

In this thesis study, design and implementation of an example railway interlocking mechanism with formal methods is aimed. German `Ks` signal system is considered as the signalling principle for designed simple interlocking. However, all features of the Ks system are not considered for the purpose of simplification of the study. All basic terms and equipment used in railway signalling are defined in the first chapter. Then, the features of `Ks` signalling system and Turkish signalling system are explained in detail.In the third chapter, definition of the interlocking is given and the functionality of the interlocking in railways is explained. Most of the definitions in third chapter are excerpted from reference number 2.In the fourth chapter, formal methods that are also used for designing interlocking system are explained. Then, two widely used formal methods, `Petri Nets` and `Finite State Machines` are discussed. Model of a simple turnstile device is given as an example to show design steps of finite state machines method. Afterwards, two different implementation software are examined with advantages and disadvantages. In the end of the chapter, implementation of example given before is achieved with both programming tools.In fifth chapter, a model railway station is created. All types operational specifications and characteristics are defined for the model station that includes train types, line types and others. Then, positioning of the signalling equipment on the model station is discussed. In `Example Interlocking Design` part, the route table of the model station is generated and a route setting mechanism is designed with using finite state machines method. Firstly, control unit of all wayside equipment are modelled and implemented. Afterwards, some basic route setting functions according to route setting rules are modelled with the same method. Finally, the route setting mechanism for the first route defined in the route table is created with developed models. Then, it is implemented with PLC programming software, SilworX, and tested with the same software.The RAMS analyses are presented in chapter 7. Basic definitions of RAMS are explained and two mostly used methods in RAMS analysis, `Fault Tree Analysis` and `Markov Model` are explained with detailed examples. Finally, a Markov model is created for the model station which is designed in fifth chapter and equations used for RAMS calculations are obtained. The RAMS parameters are estimated.Final chapter presents results and conclusion of the thesis work. Designed example interlocking and the future works are discussed in this chapter.