A Verification Approach for Programmable Logic Controllers

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