Model verification of interlocking software model

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.