Anklaşman sistemi yazılım modelinin model sınamasının yapılması

Tarihsel gelişim süreci içerisinde demiryolu trafiğinin düzenlenmesi ilk zamanlarda tamamen insan eliyle yürütülürken günümüzde elektronik sistemler tarafından otomatik olarak gerçeklenmektedir. Gelişen teknoloji neticesinde günümüzde özel olarak üretilen adanmış donanımlar üzerinde koşan yazılımlar yerini daha modüler ve esnek biçimde kullanılabilen ve daha düşük maliyetli PLC(Programmable Logic Control) tabanlı sistemlere bırakmaktadır. Anklaşman sistemlerinin SIL(Security Integrity Level) gibi ciddi güvenlik standartlarını sağlaması beklenmekte ve bu amaçla ciddi sınama eforu harcanmaktadır. Otomatik anklaşman sistemleri, günümüz demiryolu sistemlerinin işleyişinin düzenlenmesinin güvenli bir biçimde yapılmasını sağlayan en önemli bileşenlerdir. Bu sebeple, karmaşık hatlara ve yoğun tren trafiğine sahip istasyonlarda kullanılan anklaşman sistemlerinin doğru çalışacak biçimde üretilmesi büyük önem taşımaktadır. Bu tez çalışmasında, ülkemizdeki bir tren istasyonunda kullanılmakta olan PLC tabanlı bir anklaşman sistemi yazılım prototipinin biçimsel bir yöntem olan model sınama teknikleri kullanılarak doğrulanması amaçlanmaktadır. Anklaşman sistemlerinin sınanması farklı düzeylerde ve çeşitli yaklaşımlar kullanılarak gerçekleştirilmektedir. Bu düzeyler anklaşman yazılımı bileşenlerinin tabi tutulduğu birim testlerinden, gerçek sistemin bilfiil denendiği saha testlerine kadar farklılık gösterebilmektedir. Sınamaların gerçekleştirilmesindeki temel kaygı sistem çalışması sırasında oluşabilecek tüm olası durumların sınanmasının zaman ve bellek gibi mali kısıtlar nedeniyle her zaman mümkün olmamasının yanında sözü edilen olasılıkların oluşturulma işlemi de bileşen-durum sayısının büyüklüğü nedeniyle kendi içinde zorluklara sahiptir. Bu zorlukların aşılmasında çeşitli otomatik sınama yöntemleri ve durum üretim yöntemleri kullanılmakla birlikte yapılan sınamaların kapsadığı durum sayısı çoğu zaman yetersiz kalmaktadır. Anklaşman sistemleri gibi gerçek zamanlı sistemlerin sınanmasında kullanılan biçimsel yaklaşımlardan bir tanesi de model sınama yöntemleridir. Model sınamada sınanacak sistem bileşenlerinin soyut durum tabanlı modelleri oluşturularak otomatik bir biçimde sistem bileşenlerinin olası bütün durum geçiş senaryoları oluşturularak biçimsel bir şekilde ifade edilmiş sistem isterlerinin oluşturulan sistemde geçerli olup olmadığı kontrol edilmektedir. Model sınamanın avantajı üretilen soyut modellerin çeşitli detaylarda oluşturularak sistemin odaklanan belirli özellikleri üzerinde sınamalar yapılabilmesidir. Daha da önemlisi model sınama sistem çalışması esnasında oluşabilecek olası tüm durumları gözden geçirdiği için elde edilen sonuçlar modellenen sistem için "garanti" sonuçlardır ve bütün durum uzayını kapsarlar. Yapılan tez çalışmasında, PLC tabanlı oluşturulmuş anklaşman yazılımlarının durum tabanlı modellerinin oluşturulup, model sınama teknikleri ile doğrulanması için yöntemler geliştirilmesi amaçlanmaktadır. Geliştirilecek yöntemler 2009-2012 yılları arasında İTÜ ile TÜBİTAK BİLGEM ortaklığıyla gerçekleştirilmiş UDSP(Ulusal Demiryolu Sinyalizasyon Projesi) kapsamında İTÜ tarafından üretilen PLC yazılım prototipleri üzerinde denenerek geliştirilmiştir. Tez amacı olarak, otomatik anklaşman yazılımları için güvenlik garantileri verebilen bir sınama yöntemi geliştirmektir. Bu tür sınama yöntemi, sistem geliştirilmeden model üzerinde ortaya çıkaracağı kusurlar ile mali ve sistem geliştirildikten sonra ortaya çıkaracağı kusurlar ile sistem güvenliği açısından önemli faydalar sağlayacaktır.