Anklaşman Sistemi Yazılım Modelinin Model Sınamasının Yapılması

Abstract

Tarihsel gelişim süreci içerisinde demiryolu trafiğinin düzenlenmesi ilk zamanlarda tamamen insan eliyle yürütülürken günümüzde elektronik sistemler tarafından otomatik olarak gerçeklenmektedir. Gelişen teknoloji neticesinde günümüzde özel olarak üretilen adanmış donanımlar üzerinde koşan yazılımlar yerini daha modüler ve esnek biçimde kullanılabilen ve daha düşük maliyetli PLC(Programmable Logic Control) tabanlı sistemlere bırakmaktadır. Anklaşman sistemlerinin SIL(Security Integrity Level) gibi ciddi güvenlik standartlarını sağlaması beklenmekte ve bu amaçla ciddi sınama eforu harcanmaktadır. Otomatik anklaşman sistemleri, günümüz demiryolu sistemlerinin işleyişinin düzenlenmesinin güvenli bir biçimde yapılmasını sağlayan en önemli bileşenlerdir. Bu sebeple, karmaşık hatlara ve yoğun tren trafiğine sahip istasyonlarda kullanılan anklaşman sistemlerinin doğru çalışacak biçimde üretilmesi büyük önem taşımaktadır. Bu tez çalışmasında, ülkemizdeki bir tren istasyonunda kullanılmakta olan PLC tabanlı bir anklaşman sistemi yazılım prototipinin biçimsel bir yöntem olan model sınama teknikleri kullanılarak doğrulanması amaçlanmaktadır. Anklaşman sistemlerinin sınanması farklı düzeylerde ve çeşitli yaklaşımlar kullanılarak gerçekleştirilmektedir. Bu düzeyler anklaşman yazılımı bileşenlerinin tabi tutulduğu birim testlerinden, gerçek sistemin bilfiil denendiği saha testlerine kadar farklılık gösterebilmektedir. Sınamaların gerçekleştirilmesindeki temel kaygı sistem çalışması sırasında oluşabilecek tüm olası durumların sınanmasının zaman ve bellek gibi mali kısıtlar nedeniyle her zaman mümkün olmamasının yanında sözü edilen olasılıkların oluşturulma işlemi de bileşen-durum sayısının büyüklüğü nedeniyle kendi içinde zorluklara sahiptir. Bu zorlukların aşılmasında çeşitli otomatik sınama yöntemleri ve durum üretim yöntemleri kullanılmakla birlikte yapılan sınamaların kapsadığı durum sayısı çoğu zaman yetersiz kalmaktadır. Anklaşman sistemleri gibi gerçek zamanlı sistemlerin sınanmasında kullanılan biçimsel yaklaşımlardan bir tanesi de model sınama yöntemleridir. Model sınamada sınanacak sistem bileşenlerinin soyut durum tabanlı modelleri oluşturularak otomatik bir biçimde sistem bileşenlerinin olası bütün durum geçiş senaryoları oluşturularak biçimsel bir şekilde ifade edilmiş sistem isterlerinin oluşturulan sistemde geçerli olup olmadığı kontrol edilmektedir. Model sınamanın avantajı üretilen soyut modellerin çeşitli detaylarda oluşturularak sistemin odaklanan belirli özellikleri üzerinde sınamalar yapılabilmesidir. Daha da önemlisi model sınama sistem çalışması esnasında oluşabilecek olası tüm durumları gözden geçirdiği için elde edilen sonuçlar modellenen sistem için “garanti” sonuçlardır ve bütün durum uzayını kapsarlar. Yapılan tez çalışmasında, PLC tabanlı oluşturulmuş anklaşman yazılımlarının durum tabanlı modellerinin oluşturulup, model sınama teknikleri ile doğrulanması için yöntemler geliştirilmesi amaçlanmaktadır. Geliştirilecek yöntemler 2009-2012 yılları arasında İTÜ ile TÜBİTAK BİLGEM ortaklığıyla gerçekleştirilmiş UDSP(Ulusal Demiryolu Sinyalizasyon Projesi) kapsamında İTÜ tarafından üretilen PLC yazılım prototipleri üzerinde denenerek geliştirilmiştir. Tez amacı olarak, otomatik anklaşman yazılımları için güvenlik garantileri verebilen bir sınama yöntemi geliştirmektir. Bu tür sınama yöntemi, sistem geliştirilmeden model üzerinde ortaya çıkaracağı kusurlar ile mali ve sistem geliştirildikten sonra ortaya çıkaracağı kusurlar ile sistem güvenliği açısından önemli faydalar sağlayacaktır.

While, in the early days of railway interlocking, the process was achieved by total human control, today's systems are almost completely controlled by automatic electronic system and software. Moreover the dedicated hardware and specialized software being used in developing such systems is being replaced by PLC(Programmable Logic Control) based systems because of the modularity and cost effectiveness of those systems. Like every interlocking system PLC based interlocking systems also need to be heavily tested and verified to satisfy safety properties in order to meet certain safety standards like SIL(Security Integration Level). Automatic interlocking systems are the crucial components in the safe orchestration process of today's railway systems. Especially when it comes to regulating complicated train traffic in a station, the process becomes more important to ensure safety in the station. In the proposed project, verification of an interlocking system software being used in a local train station is going to be performed using model checking techniques. Verification of interlocking systems can be achieved at various levels and various verification techniques. These levels may change from unit tests applied on basic system components to the field tests, which are applied on real hardware and on actual train stations. Biggest concern on such tests are not only being unable to test every produced scenario because of time and memory constraints but also being unable to produce every meaningful testing scenario because of the unmanageable number and state space of system components. To overcome such difficulties automatic test generation tools are often used however even those tools cannot produce satisfactory results sometimes. Model checking is one of the formal methods that can be used in verification of such real-time systems. In model checking, abstract state-based models of system components are built by system designers and feed into the model checker. Model checker then produces every possible state change interleavings of those models and verify certain properties explicitly stated by means of formal specification and mostly temporal logic. One important advantage of model checking is being able to produce abstract models in various levels of detail and focus on different properties of the system in distinct verification phases. A more important advantage is providing guarantees based on the model under verification since the model checker checks every possible execution of the system under consideration. In this thesis, the aim is to develop techniques to produce abstract models from PLC software of railway interlocking systems and verify produced models using model checking. Techniques that was developed will be tested on the PLC software prototypes of the interlocking system produced by National Railway Signalization Project performed by İTÜ and TÜBİTAK BİLGEM between 2009-2012. The project aims to produce a model checking based verification system that can provide safety guarantees on the domain of PLC based interlocking which is expected to be used wider in the national railway systems. Such a system is going to provide significant benefits both in terms of cost by identifying possible defects before the interlocking software is produced and also in terms of safety by detecting defects after the interlocking system is developed. PLC software is generally used in critical systems that work as parallel and/or real-time fashion. PLC programming languages, having a simpler syntax than modern programming languages, are characteristically closer to machine instruction level. These properties frequently make them subject to the verification and model checking studies. Model checking studies can be applied over the elements (i.e. signal lights, track circuits, interlocks) of an interlocking system is presented where PLC software under verification controls and orchestrates the behavior of interlocking elements. Presented study is applied on text based PNLF(Petri Net Linear Form) representations of Petri Net models of PLC programs since Petri Nets can be used to model PLC software independent of the programming language used. By representing the PLC programs as Petri Nets and parsing PNLF documents that represent those Petri Nets, it became possible to transform the PLC programs to model checker language by the aid of computer programs. PLC programs develop via FBD(Function Block Diagram) programming language is transformed into Petri Nets. Since PNLF is a text based representation, it is used in order to process a graphical representation of Petri Net by computer. For this manner a grammer was designed for defining rules of PNLF. Those rules are processed with Java Programming language by using ANTLR(Another Tool For Language Recognition) open source library. In the rules, both petri net elements(place,transitions, tokens, etc) and some interlocking elements(signals) are represented. ANTLR is used for parsing a PNLF statement and extract all elements by the rules defined in grammer. Extracted elements are used to generate UPPAAL models for each PLC software elements(function blocks in FBD). Model checking queries also generated for each UPPAAL models. Since some PLC software elements(such as Timer On Delay) can not be transformed into petri nets, models which includes such elements are modified manually by adding some places, transitions and clock variables into UPPAAL model, but their queries are generated automatically. this modification affects state space negatively. After all UPPAAL models are automatically generated for each PLC software elements, high-level system definition is also automatically generated. After the transformation process, model checking is applied on each different interlocking system element by regarding real-time and relative-time properties. Moreover, model checking is also applied on a basic interlocking system where many interlocking system elements work in coordination. While model checking process, state explosion occured for many models. Also some limitation in UPPAAL deadlock occured for all models. Because of the state space explosion and deadlock in whole interlocking system verification a number of abstraction techniques are applied to overcome problem. Those abstraction include a nondeterministic automata and a dual automata for models generated for each PLC software elements. After applying these abstraction, model checking become possible for some models, but for other state space explosion continues. Model checking process is done in limited assumptions.