A Control Software Development Method Using IEC 61499 Function Blocks, Simulation and Formal Verification

A new control software development method is presented. It uses IEC 61499 function blocks for control software programming and provides tools for simulation, execution, automatic model generation and formal verification of the control code during the development. Simulation and execution are supported by the same tool, the Fuber runtime environment. Formal modeling is done using extended finite automata (EFA) and an automatic model generation tool. Formal verification shows the behavior of the closed-loop system. i.e. when control code is executed against the model of the process. The model can use a non-deterministic execution control chart (ECC) in the process model block. The control code and the process model are expressed using the IEC 61499 language in order to avoid maintenance of the process model and control code in different languages, thus making it easier to use the formal verification in the control software development.