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
- Tez No: 432023
- Danışmanlar: YRD. DOÇ. DR. ÖZGÜR TURAY KAYMAKÇI
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Elektrik ve Elektronik Mühendisliği, Mühendislik Bilimleri, Computer Engineering and Computer Science and Control, Electrical and Electronics Engineering, Engineering Sciences
- Anahtar Kelimeler: anklaşman tablosu, model kontrolü, ASM, Interlocking, model checking, Abstract State Machine
- Yıl: 2016
- Dil: Türkçe
- Üniversite: Yıldız Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Kontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 63
Ö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.
Özet (Çeviri)
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.
Benzer Tezler
- Raylı ulaşım sinyalizasyon sistemlerinde anklaşman algoritması tasarımı ve otomat yaklaşımı ile otomatik kod üretme
Interlocking algorithm design in railway transportation systems and automated code generation with automata approach
ARCAN SONAT
Yüksek Lisans
Türkçe
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
DOÇ. DR. MEHMET TURAN SÖYLEMEZ
- Demiryolu anklaşman sistemlerinin petri ağları ile tasarımı ve gerçeklenmesi
Railway interlocking system design and implementation using petri nets
CEM BAŞKOCAGİL
Doktora
Türkçe
2014
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
PROF. DR. SALMAN KURTULAN
- Raylı ulaşım sinyalizasyon sistemleri için otomatik anklaşman algoritması ve kodu üretme yöntemi
Automatic interlocking algorithm and code generation method for railway transportation signalization systems
SERHAT TÜRK
Yüksek Lisans
Türkçe
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
DOÇ. DR. MEHMET TURAN SÖYLEMEZ
- Demiryolu sinyalizasyon sistemlerinde anklaşman tablosu oluşturma: Başakşehir metrosu örneği
Composing a route table on railway signaling systems: Example of Basaksehir metro
MURAT ÇOLAKKADI
Yüksek Lisans
Türkçe
2013
Elektrik ve Elektronik MühendisliğiBahçeşehir ÜniversitesiKentsel Sistemler ve Ulaştırma Yönetimi Ana Bilim Dalı
PROF. DR. AHMET AKBAŞ
- A control and automation engineering approach to railway interlocking system design
Demiryolu anklaşman sistem tasarımına kontrol ve otomasyon mühendisliği yaklaşımı
MUSTAFA SEÇKİN DURMUŞ
Doktora
İngilizce
2014
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET TURAN SÖYLEMEZ