View in EDS

Automatic Model Transformation and Formal Verification for Function Block of IEC 61499.

Saved in:
Bibliographic Details
Title: Automatic Model Transformation and Formal Verification for Function Block of IEC 61499.
Authors: Chen, Yean-Ru1 (AUTHOR) chenyr@mail.ncku.edu.tw, Hsu, Chia-Hao1 (AUTHOR), Li, Tien-Fu1 (AUTHOR), Lin, Cheng-Yuan1 (AUTHOR), Weng, Shao-Chia1 (AUTHOR), Tsai, Min-Yan1 (AUTHOR)
Source: Software & Systems Modeling. Apr2026, Vol. 25 Issue 2, p615-633. 19p.
Subjects: Finite state machines, Verification of computer systems, Flow charts, Mathematical models
Abstract: The IEC 61499 standard describes the structure and behavior of distributed control systems, providing a design language at the system level and a specification for distributed systems. In the design of the control flow, the function block of the IEC 61499 standard will use an execution control chart to describe its behavior. An operation state machine is designed to describe the operation of the function block. It is necessary to consider the interaction between the execution control chart and the operation state machine for control behavior descriptions. The function block model cannot be directly used as the input of model checkers, so it needs to be transformed formally and semantically equivalently to the input models of formal verification tools. This paper proposes a method to automatically transform the function block model into a finite automata model. We use bisimulation to prove that the behavior of the transformed finite automata model is consistent with that of the function block. We further demonstrate that the transformed finite automata model is used as the input to the model checker for formal verification. [ABSTRACT FROM AUTHOR]
Copyright of Software & Systems Modeling is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:The IEC 61499 standard describes the structure and behavior of distributed control systems, providing a design language at the system level and a specification for distributed systems. In the design of the control flow, the function block of the IEC 61499 standard will use an execution control chart to describe its behavior. An operation state machine is designed to describe the operation of the function block. It is necessary to consider the interaction between the execution control chart and the operation state machine for control behavior descriptions. The function block model cannot be directly used as the input of model checkers, so it needs to be transformed formally and semantically equivalently to the input models of formal verification tools. This paper proposes a method to automatically transform the function block model into a finite automata model. We use bisimulation to prove that the behavior of the transformed finite automata model is consistent with that of the function block. We further demonstrate that the transformed finite automata model is used as the input to the model checker for formal verification. [ABSTRACT FROM AUTHOR]
ISSN:16191366
DOI:10.1007/s10270-025-01316-y