Function Blocks and Formal Verification: Systematic Modeling Approach
José Machado1; Joel Galvão1; Alexandre Fernandes1
1 University of Minho
doi:10.20906/CPS/COB-2015-1736
Resumo
Formal Verification of automation systems controllers' software is a complex task. This is, mainly, due to the fact that are necessary high skilled designers for modelling those automation systems, because the results obtained from formal verification task are highly dependent of the "quality" of the developed models for that purpose. In this paper, is explained and presented an approach for modelling some 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 simple to use and to obtain, following some systematic rules.
Palavras-chave: Software Engineering; Formal verification; Automation; Software tools; Real-Time Systems