Raylı ulaşım sistemlerinde anklaşman tablolarının doğruluğunun model kontrolü yöntemiyle test edilmesi
Verifying the accuracy of interlocking tables for signalling systems using model checking method
Yazar: BASRİ TUĞCAN ÇELEBİ
Danışman: YRD. DOÇ. DR. ÖZGÜR TURAY KAYMAKÇI
Yıldız Teknik Üniversitesi / Fen Bilimleri Enstitüsü / Kontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
Derece: Yüksek Lisans, 2016
Konu: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control ; Elektrik ve Elektronik Mühendisliği = Electrical and Electronics Engineering ; Mühendislik Bilimleri = Engineering Sciences
Dizin: Ayrık olay modelleme = Discrate event modelling ; Bilgisayar destekli modelleme = Computer aided modelling

Özet:
Raylı ulaşım sistemleri olası risklere karşı olan duyarlılığı en aza indirgeyebilmek için kullanılacak ürün, yöntem ve tekniklerin uluslararası standartlar tarafından belirlendiği kritik bir sektördür. İlgili standartlar yüksek bir emniyet seviyesine ulaşılabilmesi için geliştirme sürecinde bazı yöntemlerin kullanılmasını şiddetle tavsiye etmektedir. CENELEC 50128, Tablo A.17'de sistem modellenme aşamasında sonlu durum makinalarını ve Tablo A.5'de geliştirilen kontrol algoritmalarının doğrulama ve test aşamasında formal ispat yöntemlerinin kullanılmasını şiddetle tavsiye etmektedir. Bu kapsamda bu çalışmada sinyalizasyon sistemlerinin en kritik bölümü olan anklaşman sistemi incelenmiştir öyle ki anklaşman sistemleri geliştirilirken kodun üretilme aşamasında referans alınan anklaşman tablolarının ASM(Abstract State Machine) ile modellenmesi ve NuSMV yardımıyla model kontrolü gerçekleştirilerek doğruluğu test edilmesi ele alınmıştır. 
Bunların yanında anklaşman sistemlerinde otomatik olarak model kontrolünü yapılabilmesi için geliştirilen ASM modeli ve NuSMV kodu genelleştirilmiş bir yapıda oluşturulmuştur. 
Tasarlanan yazılım İstanbul Ulaşım A.Ş. tarafından işletilen, T4 Topkapı-Habibler hattı üzerinde bulunan "50. Yıl-Bastabya" istasyonuna ait topoloji ele alınarak düzenlenmiş ve başarılı sonuçlar elde edilmiştir.

Anahtar Kelimeler: anklaşman tablosu, model kontrolü, ASM

Abstract:
Railway transportation systems is a critical sector where products, methods and techniques to be used are identified by international standards so that susceptibility to possible risks can be reduced to minimum level. CENELEC 50128 strongly recommends the utilization of finite state machines during system modeling stage and of formal proof methods during the verification and testing stages of control algorithms. This study examines the most critical part of urban signaling systems, namely the interlocking system. It handles the F of interlocking tables, which occupy a crucial role in the production of the code, through ASM (Abstract State Machine) and testing the verification thereof by conducting model checking through NuSMV. 
In addition, ASM model and NuSMV code, developed for the purpose of performing model control automatically in interlocking systems, has been formed in a generalized structure. Consistency of the developed model has further been supervised through fault injection method. 
The software design has been arranged based on the topology of "50. Yıl Bastabya" station, operated by Istanbul Transportation Co.

Key words: Interlocking; model checking; Abstract State Machine