+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 23. September 2021, 11.00 Uhr Zoom: https://rwth.zoom.us/j/92021395779?pwd=ckRtKzJhcHFmeWxaU3YxSEZRWTJTUT09 Meeting-ID: 920 2139 5779 Kenncode: 534446 Referent: Dimitri Bohlender M.Sc. Lehrstuhl Informatik 11 Thema: Symbolic Methods for Formal Verification of Industrial Control Software Abstract: 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. My 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. In this talk, we give an overview over our contributions with a focus on the approaches that leverage constrained Horn clause solving. After a short introduction, we sketch how a logical characterisation of control software safety in terms of constrained Horn clauses can be derived from reactive systems safety foundations. 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. Furthermore, we present approaches for the design and verification of control software that is resilient to potential restarts of the controller. We show how the choice of persistent variables can be reduced to parameter synthesis, and solved by extending the previous verification procedures. Es laden ein: die Dozent*innen der Informatik