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.

This contribution defines for the first time “safety automata”, a specification language for safety control functions. This fills an important gap in the method tool box of the automation engineer. The definition has a profound potential to broaden the use of automata and their well-known advantages in industrial applications. The advantages and application of safety automata are explained by example via the function block SF_Equivalent of the PLCopen specification. Stepwise, the authors illustrate the specification of this function block by means of safety automata, the transformation rules to implement the automata in fully functional PLC code, and finally the generation of test cases that allow checking both the automata and the PLC code.

Systematic decision support for architectural design decisions is a major concern for software architects of evolving service-oriented systems. In practice, architects often analyse the expected performance and reliability of design alternatives based on prototypes or former experience. Model-driven prediction methods claim to uncover the tradeoffs between different alternatives quantitatively while being more cost-effective and less error-prone. However, they often suffer from weak tool support and focus on single quality attributes. Furthermore, there is limited evidence on their effectiveness based on documented industrial case studies. Thus, we have applied a novel, model-driven prediction method called Q-ImPrESS on a large-scale process control system consisting of several million lines of code from the automation domain to evaluate its evolution scenarios. This paper reports our experiences with the method and lessons learned. Benefits of Q-ImPrESS are the good architectural decision support and comprehensive tool framework, while one drawback is the time-consuming data collection.

Model checking of binary code is recognized as a promising tool for the verification of embedded software. Our approach, which is implemented in the [MC]SQUARE model checker, uses tailored simulators to build state spaces for model checking. Previously, these simulators have been generated by hand in a time-consuming and error-prone process. This paper proposes a method for synthesizing these simulators from a description of the hardware in an architecture description language in order to tackle these drawbacks. The application of this approach to the Atmel ATmega16 microcontroller is detailed in a case study.

Architecture-based software reliability analysis methods shall help software architects to identify critical software components and to quantify their influence on the system reliability. Although researchers have proposed more than 20 methods in this area, empirical case studies applying these methods on large-scale industrial systems are rare. The costs and benefits of these methods remain unknown. On this behalf, we have applied the Cheung method on the software architecture of an industrial control system from ABB consisting of more than 100 components organized in nine subsystems with more than three million lines of code. We used the Littlewood/Verrall model to estimate subsystems failure rates and logging data to derive subsystem transition probabilities. We constructed a discrete time Markov chain as an architectural model and conducted a sensitivity analysis. This paper summarizes our experiences and lessons learned. We found that architecture-based software reliability analysis is still difficult to apply and that more effective data collection techniques are required.

Static analysis is often performed on source code where intervals -- possibly the most widely used numeric abstract domain -- have successfully been used as a program abstraction for decades. Binary code on microcontroller platforms, however, is different from high-level code in that data is frequently altered using bitwise operations and the results of operations often depend on the hardware configuration. We describe a method that combines word- and bit-level interval analysis and integrates a hardware model by means of abstract interpretation in order to handle these peculiarities. Moreover, we show that this method proves powerful enough to derive invariants that could so far only be verified using computationally more expensive techniques such as model checking.

The interest of industries in model checking software for microcontrollers is increasing. However, there are currently no appropriate tools that can be applied by embedded systems developers for the direct verification of software for microcontrollers without the need for manual modeling. This article describes a new approach to model checking software for microcontrollers, which verifies the assembly code of the software. The state space is built using a tailored simulator, which abstracts from time, handles nondeterminism, and creates an overapproximation of the behavior shown by the real microcontroller. Within this simulator, we apply abstraction techniques to tackle the state-explosion problem. In our approach, we combine different formal methods, namely, model checking, static analysis, and abstract interpretation. We also combine explicit and symbolic model checking techniques. This article presents a case study using several programs to demonstrate the efficiency of the applied abstraction techniques and to show the applicability of this approach.

Model checking of assembly code is a promising approach to satisfy the demand for verification in nowadays ultra-high reliable embedded systems software. Frequent interaction with its environment, e.g., by sending or reading data over the microcontrollers I/O lines, lies in the nature of embedded systems. Thus, making the long-standing problem of explicit-model checking even worse, namely the state-explosion problem. This paper presents a concept to tackle these difficulties by using a 3-valued logic in the state representation and showing its benefits in terms of state-space savings whenever logic operations are executed by the target microcontroller. To highlight the effectiveness of this approach, termeddelayednondeterminismwithlookahead, an embedded program exemplifying typical microcontroller source code is analyzed and the resulting state space sizes are discussed. The introduced abstraction technique is implemented in the MCS-51 simulator component for the[mc]squaremodel checker which is developed by the RWTH Aachen University.

The paper presents details of a model checker for microcontroller-based embedded systems, called [mc] square. The purpose of the tool is to make model checking technology applicable in an embedded systems industry context. Consequently, it does not implement new theory but combines existing techniques to achieve the necessary efficiency and usability in a novel application area. One of the pragmatic requirements has been that model checking must be possible without any kind of manual preprocessing of the code. In its core, [mc]square is an explicit state, CTL model checker which builds the state space from the hardware-specific assembly code. The paper describes the tool features in detail and illustrates its abilities using two realistic examples.