Module Verifications for Function Block Based Safety-Related Industrial Control Systems

Safety-related system development is now standardized in some intimation standards such as IEC 61131, For safety-related industrial applications, we propose using Function Block concept to facilitate system specification and verification testing. Control loops are built from components taken from domain-specific function block libraries. Code inspection and testing are the two predominant quality assurance techniques. For highly dependable control applications, however, these techniques are not sufficient, in general. This paper suggests to augment testing with compositional, supported verification. The approach is based on a representation of IEC 61131-3 function blocks in higher-order logic. The verification task is separated into the a priori verification of library components and a separate proof of individual application programs.