A Tool for Verification of PLC Safety Components by Symbolic Execution (Java)
The PLCopen safety standard is a specification proposed for IEC 61131-3 for modeling and implementation of safety-related aspects. The standard specifies a set of safety components in the form of automata. This work presents an approach for verification of implementations of safety components with respect to the safety automata specifications. The approach is based on symbolic execution and works by symbolically executing the possible paths taking during control cycles. The possible paths form state of the extracted state automata and the possible sequences of execution cycles represent the possible transitions. The thesis presents the theoretical background, the implementation of the approach and the application for verifying safety components.