A Verification Approach for Programmable Logic Controllers

Conference: MBMV 2020 – Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen - GMM/ITG/GI-Workshop
03/19/2020 - 03/20/2020 at Stuttgart, Deutschland

Proceedings: GMM-Fb. 96: MBMV 2020

Pages: 3Language: englishTyp: PDF

Elfatih, Braah; Sauppe, Matthias; Heinkel, Ulrich (Chemnitz University of Technology, Professorship Circuit and System Design, 09126 Chemnitz, Germany)

This extended abstract presents first results of a research project that addresses an approach to verify the functionality of Programmable Logic Controllers (PLCs). The main feature of this technique is concentrated on its ability to automatically generate functional test cases for a test platform completely from a formal test specification without any implementation details. The resulting platform provides the environment of the PLC, consisting of the PLC testbench in Structured Text (ST) format and test patterns. The specification is modeled in a complete property set using InTerval Language (ITL), while input and output signal types are defined using VHDL. The presented algorithm uses inherent properties of the formal test specification (completeness, consistency) to automatically generate a minimal set of test cases, covering all functional states as well as corner cases.