E-Thesis 130 views 71 downloads
Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool / HARRY BRYANT
Swansea University Author: HARRY BRYANT
Abstract
Programming logic controllers (PLCs) [16] are widely used to control processes, as can be found in home appliances such as dishwashers and washing machines or in industrial applications where they control components in a production line or railway interlockings [10]. PLCs are often used to control s...
| Published: |
Swansea, Wales, UK
2023
|
|---|---|
| Institution: | Swansea University |
| Degree level: | Master of Research |
| Degree name: | MRes |
| Supervisor: | Roggenbach, Markus. and Kullmann, Oliver. |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa64905 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
Programming logic controllers (PLCs) [16] are widely used to control processes, as can be found in home appliances such as dishwashers and washing machines or in industrial applications where they control components in a production line or railway interlockings [10]. PLCs are often used to control safety critical systems. For instance, malfunctioning dishwashers and washing machines can flood kitchens and homes, malfunctioning robotic arm may lead to human injury or damage to the product, a malfunction of an interlocking computer could end in trains colliding. Therefore, there is a practical demand to verify PLCs as safe, more specifically, that their programs will remain in a set states which one considers to be safe. In the context of railway control systems, Siemens Mobility has been working on verifying the control programs of interlocking computers [51]. These programs are written in Ladder Logic, one of the three specialised programming languages for PLCs that are introduced in the IEC standard 61131 [21]. Siemens Mobility has been working alongside the Swansea Railway Verification Group verifying Ladder Logic programs for these interlocking computers and developed the Ladder Logic Verifier [87, 51] based on the Inductive Verification and Bounded Model Checking techniques. The issue with Inductive Verification and, therefore, the Ladder Logic Verifier, is that it suffers from possibly returning False Positives [51] due to a method-inherent over-approximation of the state space. This leads to an ambiguity should the verification process return that a safety property is not fulfilled: this can either be due to a False Positive or due to a mistake in the program to be analysed. Experience in verification practice suggests that this is the case for 30% to 40% out of around 240 groups of Abstract Safety Properties to be checked by Siemens. An Invariant can hopefully be used to prevent these over-approximation False Positives and allow the verification to pass, although they are labour intensive to find manually. This can be solved by applying the IC3 Algorithm [43, 44, 34]. In its current form the algorithm has been successful for the test bed of small Ladder Logic programs. However, it was proven to not scale well when tested on a Siemens industrial interlocking. This thesis presents developments in IC3 implementations that improve its efficiency so it can discover the Invariants and allow the industrial railway interlockings to pass under the Ladder Logic Verifier. |
|---|---|
| Keywords: |
Verification, IC3, Railways, SAT Solving, Ladder Logic, Invariants, Inductive Strengthening, Inductive Verification, Bounded Model Checking |
| College: |
Faculty of Science and Engineering |
| Funders: |
Siemens Mobility |