Scholarlink

<p>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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 期刊论文

  • 发表日期：

    2025年8月5日

查看全文
  • Yean-Ru Chen,
  • Chia-Hao Hsu,
  • Tien-Fu Li,
  • Cheng-Yuan Lin,
  • Shao-Chia Weng,
  • Min-Yan Tsai

摘要

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.