A formal toolchain for model-based testing of PLC systems
Chariyarupadannayil Sudheerbabu, Gaadha (2021)
Chariyarupadannayil Sudheerbabu, Gaadha
2021
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi-fe2021061537440
https://urn.fi/URN:NBN:fi-fe2021061537440
Tiivistelmä
Programmable logic controllers (PLCs) are programmable controller devices broadly used for industrial automation in industrial control systems. The correct functioning of such systems using PLCs is of utmost importance since their failure can result in financial losses and even human life losses. For the verification and validation of PLC systems, there is an increasing demand for test automation solutions. Early verification of the system’s functional and safety features based on requirements can prevent malfunctions and ensure software quality. Besides, this enhances the feedback mechanisms during the software’s development and operation phases.
Model-based testing (MBT) is a black-box testing approach that generates abstract tests automatically from a behavioral model describing the expected behavior of the system. Such model can be typically built from the requirements of the system. The quality and performance evaluation of the MBT while testing the robustness of complex systems is an area under active research.
This thesis proposes a model-based testing toolchain approach for modeling, test case generation, and test execution for safety-critical PLC systems. The proposed methodology considers the system under test as a black-box, and the behavioral model of the system is built based on the requirements specification. The model is created using UPPAAL timed automata and its properties are verified via model checking in the UPPAAL tool via Timed Computation Tree Logic (TCTL) queries. The UPPAAL tool is then used for test generation either via model checking or via structural coverage. The generated tests are executed using the Pytest testing framework against the PLC application program.
In this work, a machinery control system implemented using the IEC 61131-3’s Function Block Diagrams (FBD) programming language is used as the case study. Pytest testing framework uses OPC UA communication protocol to connect to the PLC application running on a simulated device in the CODESYS development environment. The results of the study show that the proposed toolchain can be an efficient solution for the verification of safety-critical PLC systems in the industry.
Model-based testing (MBT) is a black-box testing approach that generates abstract tests automatically from a behavioral model describing the expected behavior of the system. Such model can be typically built from the requirements of the system. The quality and performance evaluation of the MBT while testing the robustness of complex systems is an area under active research.
This thesis proposes a model-based testing toolchain approach for modeling, test case generation, and test execution for safety-critical PLC systems. The proposed methodology considers the system under test as a black-box, and the behavioral model of the system is built based on the requirements specification. The model is created using UPPAAL timed automata and its properties are verified via model checking in the UPPAAL tool via Timed Computation Tree Logic (TCTL) queries. The UPPAAL tool is then used for test generation either via model checking or via structural coverage. The generated tests are executed using the Pytest testing framework against the PLC application program.
In this work, a machinery control system implemented using the IEC 61131-3’s Function Block Diagrams (FBD) programming language is used as the case study. Pytest testing framework uses OPC UA communication protocol to connect to the PLC application running on a simulated device in the CODESYS development environment. The results of the study show that the proposed toolchain can be an efficient solution for the verification of safety-critical PLC systems in the industry.