Extending the verification coverage for PLC control programs: A functional safety approach

Programmable logic controller is becoming the most important device adopted for controlling productive systems classified as safety-related. The main reason for that is associated to advances in technology that improve the reliability of the hardware and software components of such a controller. While in the hardware context the increase in reliability is attained by using electronic components with redundancy, diversity, and low probability of failure on demand, for the safety-related software these advances are mostly dependent on the use of techniques and procedures to reduce or eliminate design errors in control programs. In this direction the IEC61508 was established, a worldwide recognized reference in functional safety that significantly contributes to the aforementioned advances. This work benefits from the recommendations of such a standard, and proposes an extension of our previous approach, where PLC control programs written in LD are modeled as extended finite state machines that are afterward formally verified. From this verification process, it is possible to identify functional errors in these machines and, consequently, the related errors in the control programs.