Skip to content
View original picture , opens in new tab/window

IEC61499 Function blocks to UPPAAL for the purpose of model checking

Published: 24 January 2017


The Aim of the project is apply the model checking verification approach to IEC 61499 function blocks in order to identify faults in the controller of a system. Once a fault is identified, it must be easily diagnosed so that the fault can then be restored and re­tested. Once a fault is restored, it must be made sure that the same fault can never occur again.


Full Description

The Functional Blocks programming model is traditionally used to program distributed industrial systems and other integrated computing systems. When such systems behave exceptionally, it may require significant effort to locate relevant program errors and provide stable fixes. Ideally, a programmer could query his/her programming environment about what caused a certain node to enter an undesired state. If sophisticated enough, such an environment could provide relevant information about the undesired behavior and propose concrete code changes.


The aim of the project is to further investigate the viability of providing such querying capabilities to modern programming environments.



  1. Design and implement a closed­loop [3] model compatible with an existing model checker (UPPAAL) reflecting the design of an existing Functional Blocks application. Initially this will be modelled manually.
  2. Define an IEC61499 translator (formal rules) that converts Functional Blocks programs into a model checker format, being in­memory or on­disk. So that model in 1, can be auto­generated in future
  3. Program (Develop) a tool-chain that can suggest how the model written in 1 might be changed in order to prevent an erroneous behavior from happening in future. This tool will interact with UPPAAL tool to check the different suggestions