Geri Dön

Designing, verification and validation of railway signaling systems using coloured petri nets

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

PDF İndir

  1. Tez No: 451016
  2. Yazar: ALI ELHAYEK
  3. Danışmanlar: PROF. DR. MEHMET TURAN SÖYLEMEZ
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2016
  8. Dil: İngilizce
  9. Üniversite: İstanbul Teknik Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Kontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: 87

Özet

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.

Özet (Çeviri)

Every weekday just in United States of America, more than 7 million people use railways in their transportation. In the same time railway is used widely as reliable freight transportation solution. So in general, railway transportation can be considered as a very vital transportation mean, this importance emerges from the fact that railways are relatively cheap and environmental friendly. This enables them to be the main transportation system in many countries. Railways systems are exposed to accidents due to huge variety of reasons like signaling system failures, human errors …etc. As railways are used by a huge number of people, the safety of railways became very important issue. This led some governments to interfere by putting standards in order to organize the operations of railway systems. CENELEC is a safety reference name which states the necessary standards of railway sector and it is composed from the following standards EN 50126, EN 50128 and EN 50129. Based on these standards, Safety Integrity Levels (SILs) were built. Signalling systems are responsible for the operations of railway systems to ensure the safety of trains and their other components. Signalling ensures optimal control for traffic in order to avoid accidents. Formal methods have a very important role in software development. Formal methods are method use the discrete mathematic techniques and tools in software and hardware development process, where the mathematical notations are used in the design and the verification of software and hardware systems. The main purpose of using formal methods is to reduce the risky consequences that can occur due to serious specification and design errors by symbolically examine the entire state space of a design Formal methods help in presenting precise record of the created software that's why it is used widely in verification and validation processes To develop software using formal method, Formal Specifications are used to describe the behavior and properties using formal language and semantics. Formal Language is used to define Rules in a precise manner. Formal language describes the grammar rules and justifies the general algorithms to be used. Semantics provide an accurate mathematical meaning to every statement. These items together will provide a formal model for the system that enables the developers to state the expected properties and then formally verify it Petri net as the models of DES. Petri net graphs depict structural information about the simple and complex systems. Coloured Petri nets are a high-level Petri nets graphical language. It is based on normal PNs, but CTL is a branching time tree; the scenarios can be symbolized by hierarchical structure in a graphical form where different scenarios can be applied. CTL* (or ASK-CTL) is used to express the state and the transition properties of the models interviewed by the state space of the coluored Petri net In this research, a signalling system for a train yard is designed by CPN. The system was verified and validated using model checking which is considered as one of the formal methods. All the processes were performed according to CENELEC to achieve minimum SIL 3.

Benzer Tezler

  1. Tez No

    106393

    Çifte kaynak kısıtlı grup teknolojisi üretim sistemlerinin bozucu faktörlere dayanıklı tasarımı

    Robust design of dual resource constrained group technology production systems

    MUSTAFA AKHUN

    Doktora

    Türkçe

    Türkçe

    1999

    Endüstri ve Endüstri Mühendisliğiİstanbul Teknik Üniversitesi

    PROF. DR. M. BÜLENT DURMUŞOĞLU

  2. Tez No

    782353

    Süpersonik hızlar için roket burnu etrafındaki akışın hesaplamalı akışkanlar dinamiği analizleri

    Computational fluid dynamics analysis of flow around the rocket nose for supersonic speeds

    AHMET SEMİH ŞİMŞEK

    Yüksek Lisans

    Türkçe

    Türkçe

    2023

    Mühendislik Bilimleriİstanbul Teknik Üniversitesi

    Makine Mühendisliği Ana Bilim Dalı

    PROF. DR. HASAN GÜNEŞ

  3. Tez No

    762985

    Parametric flow simulation for early design phase:Case study of an urban regeneration area in Izmir

    Erken tasarım aşamasında parametrik akış benzetimi: İzmir'de bir kentsel dönüşüm alanının vaka analizi

    EFE ÖNER

    Doktora

    İngilizce

    İngilizce

    2022

    Mimarlıkİzmir Yüksek Teknoloji Enstitüsü

    Mimarlık Ana Bilim Dalı

    PROF. DR. TAHSİN BAŞARAN

  4. Tez No

    545448

    Serious game development methodology with system and human oriented approach

    Sistem yaklaşımlı ve insan odaklı ciddi oyun geliştirme metodolojisi

    LEVENT BERKE ÇAPLI

    Yüksek Lisans

    İngilizce

    İngilizce

    2019

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik Üniversitesi

    Bilim ve Teknoloji Politikası Çalışmaları Anabilm Dalı

    DOÇ. DR. SERHAT ÇAKIR

  5. Tez No

    46446

    Kalite güvence sistemindeki bazı öğelerin denetim sürecine ilişkin bilgi tabanlı bir uzman sistem yaklaşımı

    Başlık çevirisi yok

    DEMET BAYRAKTAR

    Doktora

    Türkçe

    Türkçe

    1995

    Mühendislik Bilimleriİstanbul Teknik Üniversitesi

    PROF.DR. AYHAN TORAMAN

Geri Dön