Demiryolu sinyalizasyon sistemleri için renkli petri ağlarını kullanarak tasarım, doğrulama ve onaylama

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 ulaşım ve taşımanın güvenli olarak gerçekleştirilmesini sağlayan en önemli bileşen anklaşman (interlock) sistemidir. Anklaşman sisteminin geliştirilmesinde izlenilecek olan temel adımlar Avrupa Elektroteknik Standardizasyon Komitesi (European Committee for Electrotechnical Standardization - CENELEC) gibi uluslararası komiteler tarafınca hazırlanan güvenlik standartlarında tanımlanmıştır. EN 50126, EN 50128 ve EN 50129 standartlarından oluşan CENELEC, demiryolu sektöründe gerekli standartları oluşturan güvenlik referansının adıdır. Geliştirilen sinyalizasyon sisteminin istenilen Güvenlik Bütünlüğü Seviyesi (Safety Integrity Level - SIL) seviyesini sağlayabilmesi için bu güvenlik standartlarınca tavsiye edilen yöntem, teknik ve mimarilerin kullanılması yüksek önem arz etmektedir. Uluslararası güvenlik standartlarının gereksinimlerine ek olarak, sinyalizasyon sisteminin kurulacağı ülkeye ait ihtiyaçlar ve güvenlik kriterleri de göz önünde bulundurulmalıdır. Yazılım geliştirme süreci başlangıcında yazılımdan beklenen çıktılar veya başka bir deyişle yazılım isterleri oluşturulmalıdır. Sonrasında güvenlik standartlarında tavsiye edilen yöntem ve mimarilerin istenilen SIL seviyesinin sağlanabilmesi için uygun bir şekilde seçilmesi gerekmektedir. Seçilen yöntem ve mimariler yazılım isterlerini eksiksiz sağlayacak şekilde tasarımı gerçekleştirecek olan grup tarafından yazılım geliştirme sürecinde kullanılmalıdır. 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.