Symbolic methods for formal verification of industrial control software

Many of the systems that we rely on, and interact with on a daily basis, are driven by software. Unfortunately, design and implementation of such systems is naturally prone to error, as it is done by humans and involves reasoning about the vast number of states a system may reach. While testing is the common approach to alleviating the risk of writing faulty software, it can only help with finding errors, but not prove their absence. By way of contrast, formal methods have mathematical foundations, and enable rigorous reasoning about the behaviour of formally modelled systems. In particular, they give rise to formal verification procedures for proving a system's compliance with certain formal specifications. Although many such procedures can simplistically be thought of as an automatic exploration of a system's state space, the explicit enumeration of each reachable state can often be avoided. To this end, symbolic methods reason about many states at a time, by representing sets of states and transition relations as logical formulas. This thesis is concerned with advances in symbolic methods for formal verification of the software-driven reactive systems that are used in the setting of industrial automation. While these systems often operate in safety-critical environments, the specifications and peculiarities of the domain impede the use of existing verification machinery for general-purpose programming languages, leaving engineers in need of computer-aided reasoning about the control software semantics. Our contributions address this issue in platform-agnostic ways, but are presented using the example of programmable logic controllers which are tailored to the industrial automation domain and therefore widely used: (i) We propose a procedure for bounded verification of control software, where the bound denotes the number of program execution cycles instead of the traditional restriction of the number of instructions. By relating the states that are reachable at the end of each cycle through a dynamic and incremental encoding, we enable checking specifications that only refer to these observable states, while performing on par with state of the art. (ii) We derive a logical characterisation of control software safety in terms of constrained Horn clauses from reactive systems safety foundations. Leveraging solvers for this formalism is shown to be competitive with state-of-the-art approaches. To exploit the modularity of control software, the characterisation is also extended and combined with mode abstraction -- a domain-specific analysis for approximating the state space. (iii) We state a procedure for proving a module's compliance with the automaton-based specifications used by PLCopen. Unlike previous work, our approach handles calls faithfully, is incremental, compositional, and leverages Horn clause solving. (iv) We present approaches for the design and verification of control software that is resilient to potential restarts of the controller. In contrast to previous work, we do not over-approximate the program semantics and get false positives, but reason about the precise program semantics by reducing the problem to satisfiability of Horn clauses. We show how the choice of persistent variables can be reduced to parameter synthesis, and solved by extending the previous verification procedures