Demiryolu anklaşman sistemlerinin petri ağları ile tasarımı ve gerçeklenmesi
Railway interlocking system design and implementation using petri nets
Yazar: CEM BAŞKOCAGİL
Danışman: PROF. DR. SALMAN KURTULAN
İstanbul Teknik Üniversitesi / Fen Bilimleri Enstitüsü / Kontrol ve Otomasyon Mühendisliği Ana Bilim Dalı / Kontrol ve Otomasyon Mühendisliği Bilim Dalı
Derece: Doktora, 2014
Konu: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control

Özet:
Raylı ulaşım sistemlerinde güvenliğin ve sürekliliğin sağlanması esastır. Bu anlamda tren güzergâhlarında meydana gelebilecek çakışmaların engellenmesi büyük önem taşımaktadır. Trenlerin demiryolu üzerinde güvenli bir şekilde hareket edebilmesi için anklaşman sistemleri kullanılmaktadır. Çakışma probleminin giderilmesi için anklaşman sistemlerinin etkin bir şekilde tasarlanmasına ihtiyaç duyulmaktadır. Aksi takdirde anklaşman sistemlerinin tasarımında yapılacak en ufak hata bile raylı ulaşım sistemlerinin güvenliğini tehlikeye atacaktır. Anklaşman sistemlerinin etkin bir şekilde tasarlanıp gerçeklenmesi bu tezin ana konusunu oluşturmaktadır.
Bu tez çalışmasında anklaşman sistemlerinin etkin bir şekilde tasarlanması ve gerçeklenmesi için Petri Ağları'nın kullanımı üzerinde durulmaktadır. Bunun için öncelikle Petri Ağları'nın tasarımsal amaçlı kullanımı ile ilgili bilgi altyapısı oluşturulmaktadır. Ardından Petri Ağları'nın modelleme yeteneğini arttırmak için tanımlanmış olan yay türleri ele alınmakta ve bu yay türlerinin hepsini içeren Petri Ağları'nın matematiksel olarak ifade edilebilmesi için "genelleştirilmiş durum denklemi" adı altında yeni bir durum denklemi önerisi ortaya atılmaktadır. 
Anklaşman sisteminin gerçeklenmesi için PLC kullanılacaktır. Dolayısıyla anklaşman sistemi için oluşturulacak Petri Ağları modelinin PLC koduna dönüştürülmesi gerekecektir. Yapılan literatür taraması sonucunda PLC koduna dönüşüm için Petri Ağları'nın sadece grafiksel özelliklerinin kullanıldığı görülmüştür. Programlamaya uygun bir altyapı sağlanabilmesi amacıyla PLC koduna dönüşüm işlemi için Petri Ağları'nın matematiksel özelliklerinin kullanılması gerekmektedir. Tezde bu amaca hizmet eden bir yöntem önerisinde bulunulmaktadır. Bu yöntem ile Petri Ağları'nın sistem matrisinden PLC koduna doğrudan dönüşüm sağlanabilmektedir. Aynı zamanda önerilen yöntem ile sistemlerde sıklıkla karşılaşılan çığ etkisinin giderilmesi de sağlanmaktadır. Bununla birlikte yöntemin hızlı ve kolay şekilde uygulanabilmesi için tez kapsamında geliştirilen yazılım tanıtılmakta ve bu yazılımın kullanımı gösterilmektedir. Bu yazılım sayesinde Petri Ağları'nın PLC koduna dönüşümü otomatik olarak gerçekleştirilebilmektedir.
Bu tez çalışmasında önerilen yöntemin uygulanabilmesi için gerçek bir tren istasyonu ele alınmaktadır. Öncelikle bu tren istasyonuna ait anklaşman sistemi Petri Ağları ile modüler bir yaklaşım kullanılarak modellenmektedir. Bu amaçla anklaşman sistemi bir takım alt sistemlere bölünmekte ve bu alt sistemlerin her biri ayrı ayrı Petri Ağları ile modellenmektedir. Alt sistemlere ait her bir Petri Ağları modelinin PLC koduna dönüştürülmesi için önerilen yöntem kullanılmaktadır. Böylelikle anklaşman sisteminin Petri Ağları kullanılarak tasarlanması ve gerçeklenmesi sağlanmaktadır. Son olarak gerçeklenen anklaşman sisteminin test edilmesi amacıyla geliştirilen SCADA uygulaması üzerinde sistemin davranışı gözlemlenerek yapılan gerçekleme doğrulanmaktadır.

Abstract:
It is vital to provide safety and availability of the railway transportation systems. For serving such a purpose, route conflicts should be prevented in the first place. However, railway transportation systems are complex in nature and this makes it hard to accomplish such a task. That is where railway interlocking systems come into play. Interlocking systems are utilized so that trains can safely move on the railway. This can only be achieved by an efficiently designed interlocking system. Otherwise, any simple flaw in the design would lead to route conflicts, thus rendering the railway transportation system unsafe. Efficient design and implementation of railway interlocking systems constitutes the main subject of this study.
In this thesis, Petri Nets would be used for designing and implementation of interlocking systems. Petri Nets is a modeling tool that is able to represent systems both visually and mathematically. Visual aspects of Petri Nets are utilized to model the general structure of a system. Nevertheless, mathematical aspects of Petri Nets are used to realize the system dynamics. Petri Nets makes it possible to represent the system behavior mathematically via state equation. One can exploit mathematical features of Petri Nets to perform modeling, simulation, testing and verification of systems.
In order to model large-scale systems using Petri Nets, particular enhancements have become necessary to overcome arising shortfalls and to improve modeling capability. Modular Petri Nets is introduced to model complex systems in modular way. This is useful for simplifying the investigation of the system. Colored Petri Nets is proposed to make it easy to keep track of specific events taking place within the system. Timed Petri Nets is created to represent time-dependent events in the system. Together with these enhancements, Petri Nets has become more powerful modeling tool.
Specific arc types are defined to further enhance the modeling capability of Petri Nets. Inhibitor arcs are defined to enable a certain transition to take precedence over the other transitions. Using inhibitor arcs, it becomes possible to visually represent prioritization mechanism in Petri Nets. Enabling arcs are introduced to keep tokens in the input places while triggering the transition. An enabling arc is very similar to an ordinary arc. The only difference is the fact that when a transition is triggered, there is no token removal from the input place(s) connected to enabling arc(s). Nullifier arcs are proposed to remove all of the tokens from an input place at once when a transition is triggered. This functionality is used to implement the resetting mechanism in Petri Nets.
In the literature, the state equation for Petri Nets is used to model and analyze systems mathematically. However, there are not any formalized state equations defined in order to cover inhibitor, enabling and nullifier arcs. Therefore, we do not have the opportunity to represent the systems mathematically when these types of arcs are involved. In this thesis, the state equation for Petri Nets is revisited and modified to obtain a novel state equation called "generalized state equation". This state equation can be used to mathematically represent the behavior of inhibitor, enabling and nullifier arcs. Besides, software is developed and utilized to demonstrate the application of generalized state equation on an industrial automation system.
Railway signalization systems play a major role in providing safety and reliability for the railway transportation systems. The main purpose of railway signalization systems is to prevent train collisions from happening. A railway signalization system is composed of three main elements such as traffic control center, interlocking system and the field equipments. 
Traffic control center is responsible for management and observation of the entire railway traffic. Route requests are created and train positions, switch positions, signal states are observed by traffic control center. There is a two-way communication between the traffic control center and the interlocking system. Route requests originated by the traffic control center is sent to the interlocking system and at the same time the status information coming from the field equipments is sent by the interlocking system to the traffic control center. As a result of this information exchange, the interlocking software processes the route requests and these requests are either accepted or rejected regarding the status of the field equipments. Interlocking software only accepts route requests that do not lead to train collisions.
Interlocking system both gathers information from and sends commands to the field equipments. The field equipments form the infrastructure of the railway signalization system. The field equipments are composed of switches, track circuits and signals. Switches are mechanical devices that enable trains to change direction. Generally, switches have two positions such as "normal" and "reverse". When a switch is in "normal" position, train crossing over this switch does not change its direction, whereas in "reverse" position switch causes train crossing over it to change its direction. Track circuits inform the interlocking system about the existence of a train on the railway. Signals are used to inform trains about whether the railway is occupied or not. "Red" light means the railway is occupied, whereas "green" light means the railway is free.
The interlocking system is the decision maker in a railway signalization system. The main task of the interlocking system is to evaluate route requests coming from the traffic control center. During this evaluation, existing route requests and status of the field equipments are considered by the interlocking system. As a result, reasonable requests are accepted and the field equipments are locked accordingly to apply these requests. Unsuitable requests that cause collisions are rejected and are not applied. Interlocking system uses interlocking table to make these decisions. Interlocking table has entries for all of the possible routes and each of these entries identifies the conditions under which the corresponding route request should be accepted.
It is clear that the reliability of a railway signalization system is directly related to the interlocking system. Therefore, safety standards called EN50126, EN50128 and EN50129 are established by CENELEC to define general safety requirements for the railway interlocking systems. Both the hardware and the software components of an interlocking system must fulfill these standards. It is essential to use formal methods for the design of the software in order to meet these security standards.
In this thesis, the interlocking system would be implemented using PLC. In order to accomplish this task, at first, the interlocking system would be modeled using Petri Nets. Then, this Petri Nets model would have to be converted into PLC code. During literature research, it is observed that only visual aspects of Petri Nets are used for such a conversion process. And also, in the literature, there are not any available studies that exploit mathematical aspects of Petri Nets in order to realize interlocking systems using PLC code that is defined in IEC 61131-3 standards. In order to maintain an infrastructure that is favorable for programming, mathematical aspects of Petri Nets should be used for the conversion process. In this thesis, an efficient method is proposed to make the conversion from mathematical model of Petri Nets into PLC code that is defined in IEC 61131-3 standards. Then, this method is used to implement the interlocking system with PLC. In this method, conversion of Petri Nets into PLC code is directly accomplished by making use of the incidence matrix. At the same time, the proposed method also provides elimination of avalanche effect from which most of the systems suffer. In addition, software is developed to implement this methodology and usage of this software is shown on a case study. One can use this software to perform conversion of Petri Nets into PLC code automatically.
In this study, in order to apply aforementioned method, a real-life railway station is considered. At first, the interlocking system of this station is designed modularly using Petri Nets. Modularity is provided by means of partitioning the interlocking system into subsystems. Then each of these subsystems is modeled using Petri Nets, which is further converted into PLC code using proposed methodology. This concludes design and implementation of the interlocking system using Petri Nets. Finally, SCADA application is developed to test the interlocking system and on this application, the implementation of this interlocking system is verified.