Return to search

Simple Open-Source Formal Verification of Industrial Programs

Industrial programs written on Programmable Logic Controllers (PLCs) have become an essential component of many modern industries, including automotive, aerospace, manufacturing, infrastructure, and even amusement parks. As these safety-critical systems become larger and more complex, ensuring their continuous error-free operation has become a significant and important challenge. Formal methods are a potential solution to this issue but have traditionally required substantial time and expertise to deploy. This usability issue is compounded by the fact that PLCs are highly proprietary and have substantial licensing costs, making it difficult to learn about or deploy formal methods on them.
This thesis presents the OPPP (Open-source Proving of PLC Programs) system as a solution to this usability issue. The OPPP system allows the end-to-end creation and verification of PLC programs from within the development environment. The system is created with an emphasis on being easy to use, with formal constraints presented in English phrases that require no special knowledge to understand. The system uses entirely open-source components, including modified versions of both the OpenPLC development environment and the PLCverif verification platform. The OPPP system is then demonstrated to formalize the requirements of two college-level introductory PLC programming problems. It is further demonstrated to correctly find errors in and verify the correctness of a known good and known bad solution to each problem.

Identiferoai:union.ndltd.org:CALPOLY/oai:digitalcommons.calpoly.edu:theses-4228
Date01 March 2023
CreatorsPeterson, Christopher Disney
PublisherDigitalCommons@CalPoly
Source SetsCalifornia Polytechnic State University
Detected LanguageEnglish
Typetext
Formatapplication/pdf
SourceMaster's Theses

Page generated in 0.0019 seconds