Model Checking PLC Software Written in Function Block Diagram

The development of Programmable Logic Controllers (PLCs) in the last years has made it possible to apply them in ever more complex tasks. Many systems based on these controllers are safety-critical, the certification of which entails a great effort. Therefore, there is a big demand for tools for analyzing and verifying PLC applications. Among the PLC-specific languages proposed in the standard IEC 61131-3, FBD(Function Block Diagram) is a graphical one widely used in rail automation. In this paper, a process of verifying FBDs by the NuSMV model checker is described. It consists of three transformation steps: FBD→TextFBD→tFBD→NuSMV. the novel step introduced here is the second one: it reduces the state space dramatically so that realistic application components can be verified. The process has been developed and tested in the area of rail automation, in particular interlocking systems. As a part of the interlocking software, a typical point logic has been used as a test case.