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
Contract Based Verification of IEC 61499
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
CISTER, INESC TEC, ISEP.
CISTER, INESC TEC, ISEP.
Number of Authors: 4
2017 (English)In: IEEE International Conference on Industrial Informatics (INDIN), Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017, 132-141 p., 7819147Conference paper, Published paper (Refereed)
Abstract [en]

The IEC 61499 standard proposes an event drivenexecution model for component based (in terms of FunctionBlocks), distributed industrial automation applications. However,the standard provides only an informal execution semantics, thusin consequence behavior and correctness relies on the designdecisions made by the tool vendor. In this paper we presentthe formalization of a subset of the IEC 61499 standard inorder to provide an underpinning for the static verification ofFunction Block models by means of deductive reasoning. Specifically,we contribute by addressing verification at the component,algorithm, and ECC levels. From Function Block descriptions, enrichedwith formal contracts, we show that correctness of componentcompositions, as well as functional and transitional behaviorcan be ensured. Feasibility of the approach is demonstrated bymanually encoding a set of representative use-cases in WhyML,for which the verification conditions are automatically derived(through the Why3 platform) and discharged (using automaticSMT-based solvers). Furthermore, we discuss opportunities andchallenges towards deriving certified executables for IEC 61499models.

Place, publisher, year, edition, pages
Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017. 132-141 p., 7819147
Series
IEEE International Conference on Industrial Informatics INDIN, ISSN 1935-4576
National Category
Embedded Systems
Research subject
Industrial Electronics
Identifiers
URN: urn:nbn:se:ltu:diva-59756DOI: 10.1109/INDIN.2016.7819147ISI: 000393551200017Scopus ID: 2-s2.0-85012929062ISBN: 9781509028702 (electronic)OAI: oai:DiVA.org:ltu-59756DiVA: diva2:1037300
Conference
IEEE International Conference on Industrial Informatics 2016 (INDIN 2016), Poitiers, France, 18-21 July 2016
Available from: 2016-10-14 Created: 2016-10-14 Last updated: 2017-10-19Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 228 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