Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of IEC61499 Function Blocks with Abstract State Machines and SMV -- Modelling
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0003-2936-4185
University of Auckland, Penza State University, Department of Computer Science, University of Penza, Computer Science Department, Penza State University, Penza.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0002-9315-9920
Number of Authors: 3
2015 (English)In: IEEE TrustCom-BigDataSE-ISPA 2015: Helsinki, 20-22 Aug. 2015, Piscataway, NJ: IEEE Communications Society, 2015, Vol. 3, p. 313-320, article id 7345666Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE Communications Society, 2015. Vol. 3, p. 313-320, article id 7345666
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-32663DOI: 10.1109/Trustcom.2015.650ISI: 000380431400045Scopus ID: 84969132840Local ID: 73823e11-9167-417d-a059-923ab1f4f53cISBN: 9781467379519 (print)OAI: oai:DiVA.org:ltu-32663DiVA, id: diva2:1005897
Conference
IEEE TrustCom-BigDataSE-ISPA : 20/08/2015 - 22/08/2015
Note

Validerad; 2016; Nivå 1; 2016-10-10 (andbra)

Available from: 2016-09-30 Created: 2016-09-30 Last updated: 2018-04-03Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Patil, SandeepVyatkin, Valeriy
By organisation
Computer Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 32 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf