Automated verification of function block-based industrial control systems

The international standard IEC 61131-3, which supports Brad Cox’ concept of “Software-ICs” for industrial control programming, is increasingly being used in safety-related application domains. They include safety-instrumented functions, such as burner management, emergency shutdown and gas leak detection, but also complex automation processes controlling, e.g., chemical production plants. For such highly dependable applications, code inspection and testing, the predominant quality assurance techniques used in practice today, are, in general, not sufficient to demonstrate the functional correctness and safety of an application. This paper presents a theorem prover-based verification technique as a supplementary validation measure. The verification task is separated into the a priori verification of reusable function blocks, which are usually maintained in domain-specific libraries, and a separate compositional proof of individual application programs. Core concepts of the standardized languages, their semantic embedding into higher order logic, and the verification approach are illustrated with a small example. Some design ideas for a verification tool usable by automation engineers and safety licensing authorities conclude the contribution.