A Verification Approach for Programmable Logic Controllers

Abstract

This paper presents an iterative approach to the verification of programmable logic controllers. We explore the modeling method for timing, environment and controller logics in a system, in which predicate abstraction and counterexample-guided refinement strategies are employed. We use a representative example to illustrate the proposed approach and verify it by the model checker CBMC. The experimental results show the validity of the approach.