Formal Specification and Verification of Industrial Control Logic Components

Component-based programming frameworks for industrial control logic development promise to shorten development and modification times, and to reduce programming errors. To get these benefits, it is, however, important that the components are specified and verified to work properly. This work introduces Reusable Automation Components (RACs), which contain not only the implementation details but also a formal specification defining the correct use and behaviour of the component. This formal specification uses temporal logic to describe time-related properties and has a special structure developed to meet industrial control needs. The RAC can be formally verified, to determine whether the implementation fulfils the specification or not. A RAC prototype development tool has been developed to demonstrate this capability. The main difference between the RAC and other frameworks for formal verification of control logic is the specification modeling. In RAC, not only the implementation but also the specification is based on the structure and languages of conventional control logic, aiming at being easy to comprehend for control logic engineers. Several industrial examples are discussed in this paper, showing the benefits and potential of the framework.