No Cover Image

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...

Full description

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!
first_indexed 2023-11-02T14:03:01Z
last_indexed 2023-11-02T14:03:01Z
id cronfa64905
recordtype RisThesis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>64905</id><entry>2023-11-02</entry><title>Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool</title><swanseaauthors><author><sid>960a5c8f16fcc44456e20173d1ea2e1c</sid><firstname>HARRY</firstname><surname>BRYANT</surname><name>HARRY BRYANT</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2023-11-02</date><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.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea, Wales, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>Verification, IC3, Railways, SAT Solving, Ladder Logic, Invariants, Inductive Strengthening, Inductive Verification, Bounded Model Checking</keywords><publishedDay>11</publishedDay><publishedMonth>10</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-10-11</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Roggenbach, Markus. and Kullmann, Oliver.</supervisor><degreelevel>Master of Research</degreelevel><degreename>MRes</degreename><degreesponsorsfunders>Siemens Mobility</degreesponsorsfunders><apcterm/><funders>Siemens Mobility</funders><projectreference/><lastEdited>2023-11-02T14:04:13.3990294</lastEdited><Created>2023-11-02T13:58:34.6977040</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>HARRY</firstname><surname>BRYANT</surname><order>1</order></author></authors><documents><document><filename>64905__28919__67390fc425684b738a8b1c32cd839539.pdf</filename><originalFilename>2023_Bryant_H.final.64905.pdf</originalFilename><uploaded>2023-11-02T14:03:23.9403124</uploaded><type>Output</type><contentLength>19722081</contentLength><contentType>application/pdf</contentType><version>E-Thesis – open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The Author, Harry Bryant, 2023.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling v2 64905 2023-11-02 Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool 960a5c8f16fcc44456e20173d1ea2e1c HARRY BRYANT HARRY BRYANT true false 2023-11-02 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. E-Thesis Swansea, Wales, UK Verification, IC3, Railways, SAT Solving, Ladder Logic, Invariants, Inductive Strengthening, Inductive Verification, Bounded Model Checking 11 10 2023 2023-10-11 COLLEGE NANME COLLEGE CODE Swansea University Roggenbach, Markus. and Kullmann, Oliver. Master of Research MRes Siemens Mobility Siemens Mobility 2023-11-02T14:04:13.3990294 2023-11-02T13:58:34.6977040 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science HARRY BRYANT 1 64905__28919__67390fc425684b738a8b1c32cd839539.pdf 2023_Bryant_H.final.64905.pdf 2023-11-02T14:03:23.9403124 Output 19722081 application/pdf E-Thesis – open access true Copyright: The Author, Harry Bryant, 2023. true eng
title Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool
spellingShingle Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool
HARRY BRYANT
title_short Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool
title_full Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool
title_fullStr Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool
title_full_unstemmed Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool
title_sort Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool
author_id_str_mv 960a5c8f16fcc44456e20173d1ea2e1c
author_id_fullname_str_mv 960a5c8f16fcc44456e20173d1ea2e1c_***_HARRY BRYANT
author HARRY BRYANT
author2 HARRY BRYANT
format E-Thesis
publishDate 2023
institution Swansea University
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2023-10-11T14:04:22Z
_version_ 1781461273515393024
score 11.013641

Similar Items