Presentation: Formal Methods for Industrial Control Applications

Abstract

In industry, automation and control tasks are frequently operated using programmable logic controllers (PLCs). Currently, formal methods do not play an important role when developing the control software executed by PLCs, although they are often used to implement safety-critical functionality in machines or production plants. The talk describes the experience of applying model checking and static code analysis to real-world control applications according to the IEC 61131-3 standard. It is based on a multi-year collaboration between ABB corporate research and RWTH Aachen University.  Different techniques and formalisms were evaluated in the ARCADE.PLC (Aachen Rigorous Code Analysis and Debugging Environment for PLCs) framework using control code provided by ABB. While it could be shown that model checking and static code analysis of industrial size control applications is possible, not all techniques for general purpose programming languages are directly applicable. The talk discusses the tradeoffs and results for the different analysis mechanisms. It concludes with a summary of ongoing research to improve the development process of industrial control applications.