Formal verification considering a systematic modeling approach for function blocks

Formal verification of automation systems controller software is a complex task. This happens mainly because this kind of systems need to be programmed by highly skilled designers as results obtained from formal verification are highly dependent of the "quality'' of the developed models. In this paper, is explained and presented an approach for modeling a series of function blocks from IEC 61 131-3 standard and, in the same context, is proposed an approach for developing the respective Timed Automata model for formal verification purposes, by model-checking, using UPPAAL model-checker. Some interesting results are achieved and the proposed approach is user friendly.The authors are grateful to MEtRICs Research Centre for their support to this project.