On controller and plant modeling for model-based formal verification

The acceptance of formal methods in industry is a challenging task mainly due to difficult learning process and the lack of the tools and methods helping control engineer to interpret the results of formal verification procedure. We model existing source code of the controller and controller related information (controller model) along with controlled object (plant model) and verify modeled system by means of model-checking. This paper focuses on the issues related to controller and plant modeling. Ladder logic modeling is discussed along with the problems related to the plant modeling