Formal Verification of IEC61499 Function Blocks with Abstract State Machines and SMV -- Modelling

IEC 61499 Standard for Function Blocks Architecture is an executable component model for distributed embedded control system design that combines block diagrams and state machines. This paper proposes rules for formal modelling of IEC61499 function blocks for popular model checking environment of SMV using Abstract State Machines as an intermediate model. This paper first proposes a formal description of the IEC 61499 in abstract state machines (ASM). The formal description for main artifact of the standard (function block) is presented in the paper. The ASM model is further translated to the input format of the SMV model checker which is used to formally verify properties of applications developed in IEC 61499 standard. In this way the proposed verification framework enables the formal verification of the IEC 61499 control systems. The paper also highlights the other uses of verification such as portability of IEC 61499 based control applications across different implementation platforms compliant with the IEC 61499 standard. The formal model is applied on an example IEC 61499 controller, and the SMV model for the Basic Function block is explained in detail.