Formal Specification and Verification of Components for Industrial Logic Control Programming

Component based approaches to develop industrial logic control programs promise to shorten development and modification times, and to lessen programming errors. However, to get these benefits it is important that components verified to work properly are reused. This work proposes using Reusable Automation Components (RACs), which contain not only the implementation but also a formal specification defining the correct use and behaviour of the component. This specification uses temporal logic to describe relations over time. The specification is helpful both for users of the components and for developers since the complete RAC including the specification can be translated into input to a tool for formal verification, to determine whether the specification is fulfilled or not. This paper shows how the RAC can be both implemented and specified using the common IIEC 61131 standard and Ladder Diagrams. An industrial example is presented, specified and formally verified. It shows that RACs may help the developers to find errors and inconsistencies within the components, making it easier to do modifications of the code.