In industrial automation, the control and operation of factories and plants in usually performed by Programmable Logic Controllers (PLCs). As automation tasks find their way into more and more smaller application areas where it is economically not reasonable to employ, engineer and maintain a full, hardware-based PLC, a cloud-based software PLC (Soft-PLC) can serve as a Control-as-a-Service solution. In this paper, we address the question how a Soft-PLC can be augmented with cloud-required aspects such as elastic scalability and multi-tenancy. We introduce an architecture that realizes these properties and allows for the implementation of a multi-tenant, horizontally scalable Soft-PLC. Furthermore, we evaluate the most important quality attributes, i.e. Roundtrip times and scalability of our architecture based on a prototypical implementation and a case study from the building automation domain. Finally, we present lessons learned and give an outlook to further realistic scenarios for cloud-based control in industrial applications.

This paper presents a method for automatic test case generation for PLC software following the IEC61131-3 standard. The core component is a model checker that iteratively creates program traces, each of them covering a part of the program in terms of a coverage metric. These test cases are translated into Structured Text, a programming languages defined in the IEC61131-3, to allow the execution on a soft-PLC or the actual hardware. Our approach is evaluated on a set of function blocks that are used in industry. We demonstrate that test cases can be automatically generated within few seconds in most cases.

Static code analysis techniques are a well-established tool to improve the efficiency of software developers and for checking the correctness of safety-critical software components. However, their use is often limited to general purpose or “mainstream” programming languages. For these languages, static code analysis has found its way into many integrated development environments and is available to a large number of software developers. In other domains, e. g., for the programming languages used to develop many industrial control applications, tools supporting sophisticated static code analysis techniques are rarely used. This paper reports on the experience of the authors while adapting static code analysis to a software development environment for engineering the control software of industrial process automation systems. The applicability of static code analysis for industrial controller code is demonstrated by a case study using a real-world control system.

Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, both classical categories are not optimized for bug detection, where speed and precision are important, but soundness (no missed bugs) and completeness (no false positives) do not necessarily need to be guaranteed.

This paper introduces Arcade.PLC, a verification platform for programmable logic controllers (PLCs). The tool supports static analysis as well as ACTL and past-time LTL model checking using counterexample-guided abstraction refinement for different programming languages used in industry. In the underlying principles of the framework, knowledge about the hardware platform is exploited so as to provide efficient techniques. The effectiveness of the approach is evaluated on programs implemented using a combination of programming languages.