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: Elektrik ve Elektronik Mühendisliği, Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Mühendislik Bilimleri, Electrical and Electronics Engineering, Computer Engineering and Computer Science and Control, Engineering Sciences
- Anahtar Kelimeler: anklaşman tablosu, model kontrolü, ASM, Ayrık olay modelleme, Bilgisayar destekli modelleme, Interlocking, model checking, Abstract State Machine, Discrate event modelling, Computer aided modelling
- 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ı: Belirtilmemiş.
Ö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
- Kan basıncı değişiminin böbrek dokusunda gösterdiği histolojik farklılaşmalar
Renal tissue alternations caused by a change in the blood pressure
BİLGE ONARLIOĞLU(TÖREL)
Tıpta Uzmanlık
Türkçe
1987
MorfolojiCumhuriyet ÜniversitesiMorfoloji Ana Bilim Dalı
DOÇ. DR. ERDOĞAN GÜRSOY
- Geçmişten günümüzde epilepsi (sar'a)
Today and in the past of epilepsy
ÖMÜR ŞAYLIGİL
Yüksek Lisans
Türkçe
1987
Deontoloji ve Tıp TarihiUludağ ÜniversitesiDeontoloji ve Tıp Tarihi Ana Bilim Dalı
DOÇ. DR. AYŞEGÜL DEMİRHAN ERDEMİR
- Pazarlamada standardizasyonun yeri yaş meyve ve sebze ihracatında standardizasyonun önemi üzerinde bir inceleme
Başlık çevirisi yok
RECAİ ÇINAR
- Kamuya açık ortamlarda video izleme olgusunun kitle açısından irdelenmesi
Başlık çevirisi yok
ABDÜLKADİR CANDEMİR