Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
A Formal Perspective on IEC 61499 Execution Control Chart Semantics
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Embedded Internet Systems Lab.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Embedded Internet Systems Lab.ORCID iD: 0000-0002-1791-535X
ISEP, Instituto Superior de Engenharia do Porto.
ISEP, Instituto Superior de Engenharia do Porto.
Number of Authors: 4
2015 (English)In: 2015 IEEE Trustcom/BigDataSE/ISPA: Helsinki, 20-22 Aug. 2015, Piscataway, NJ: IEEE Communications Society, 2015, 293-300 p., 7345663Conference paper, Published paper (Refereed)
Abstract [en]

The IEC 61499 standard proposes an event driven execution model for distributed control applications for which an informal execution semantics is provided. Consequently, run-time implementations are not rigorously described and therefore their behavior relies on the interpretation made by the tool provider. In this paper, as a step towards a formal semantics, we focus on the Execution Control Chart semantics, which is fundamental to the dynamic behavior of Basic Function Block elements. In particular we develop a well-formedness criterion that ensures a finite number of Execution Control Chart transitions for each triggering event. We also describe the first step towards the mechanization of the well-formedness checking algorithm in the Coq proof-assistant so that, ultimately, we are able to show, once andforall,thatthisalgorithmiseffectivelycorrectwithrespectto our proposed execution semantics. The algorithm is extractable from the mechanization in a correct-by-construction way, and can be directly incorporated in certified toolchain for analysis, compilation and execution of IEC 61499 models. As a proof of concept a prototype tool RTFM-4FUN has been developed. It performs well-formedness checks on Basic Function Blocks using the extracted algorithm’s code.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE Communications Society, 2015. 293-300 p., 7345663
National Category
Embedded Systems
Research subject
Embedded System
Identifiers
URN: urn:nbn:se:ltu:diva-37870DOI: 10.1109/Trustcom.2015.647ISI: 000380431400042Local ID: c097e775-e03c-4aa5-9bac-9046db7769deISBN: 9781467379519 (print)OAI: oai:DiVA.org:ltu-37870DiVA: diva2:1011368
Conference
IEEE International Symposium on Parallel and Distributed Processing with Applications : 20/08/2015 - 22/08/2015
Note

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

Available from: 2016-10-03 Created: 2016-10-03 Last updated: 2017-11-25Bibliographically approved

Open Access in DiVA

fulltext(280 kB)33 downloads
File information
File name FULLTEXT01.pdfFile size 280 kBChecksum SHA-512
3c4c8ce3c2b7a0c21438efb7da5db37368c822c1551c48315ef598599bc8c6f1545b2af36d744bf6ab2fe44579e8f8820597140ca70679f36efb602e288a1e9c
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Lindgren, PerLindner, Marcus
By organisation
Embedded Internet Systems Lab
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 33 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • 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