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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 192418424
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Automatic Model Transformation and Formal Verification for Function Block of IEC 61499.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Chen%2C+Yean-Ru%22">Chen, Yean-Ru</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> chenyr@mail.ncku.edu.tw</i><br /><searchLink fieldCode="AR" term="%22Hsu%2C+Chia-Hao%22">Hsu, Chia-Hao</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Li%2C+Tien-Fu%22">Li, Tien-Fu</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Lin%2C+Cheng-Yuan%22">Lin, Cheng-Yuan</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Weng%2C+Shao-Chia%22">Weng, Shao-Chia</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Tsai%2C+Min-Yan%22">Tsai, Min-Yan</searchLink><relatesTo>1</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Software+%26+Systems+Modeling%22">Software & Systems Modeling</searchLink>. Apr2026, Vol. 25 Issue 2, p615-633. 19p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Finite+state+machines%22">Finite state machines</searchLink><br /><searchLink fieldCode="DE" term="%22Verification+of+computer+systems%22">Verification of computer systems</searchLink><br /><searchLink fieldCode="DE" term="%22Flow+charts%22">Flow charts</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+models%22">Mathematical models</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=192418424
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10270-025-01316-y
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 19
        StartPage: 615
    Subjects:
      – SubjectFull: Finite state machines
        Type: general
      – SubjectFull: Verification of computer systems
        Type: general
      – SubjectFull: Flow charts
        Type: general
      – SubjectFull: Mathematical models
        Type: general
    Titles:
      – TitleFull: Automatic Model Transformation and Formal Verification for Function Block of IEC 61499.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Chen, Yean-Ru
      – PersonEntity:
          Name:
            NameFull: Hsu, Chia-Hao
      – PersonEntity:
          Name:
            NameFull: Li, Tien-Fu
      – PersonEntity:
          Name:
            NameFull: Lin, Cheng-Yuan
      – PersonEntity:
          Name:
            NameFull: Weng, Shao-Chia
      – PersonEntity:
          Name:
            NameFull: Tsai, Min-Yan
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 04
              Text: Apr2026
              Type: published
              Y: 2026
          Identifiers:
            – Type: issn-print
              Value: 16191366
          Numbering:
            – Type: volume
              Value: 25
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Software & Systems Modeling
              Type: main
ResultId 1