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 Modelling and Verification of IEC61499 Function Blocks with Abstract State Machines and SMV: Execution Semantics
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.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0002-9315-9920
2015 (English)In: Dependable Software Engineering: Theories, Tools, and Applications : First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings / [ed] Xuandong Li; Zhiming Liu; Wang Yi, New York: Encyclopedia of Global Archaeology/Springer Verlag, 2015, p. 300-315Conference 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 approach to formal modelling of IEC61499 function block execution semantics for popular model checking environment of SMV using Abstract State Machines. An operational semantics of IEC 61499 application with two-stage synchronous execution model is presented using this framework. This paper first introduces the importance of model checking function block applications in different execution semantics. It highlights the uses of formal verification, such as, verifying portability (behavior) of component based control applications across different implementation platforms compliant with the IEC 61499 standard. The formal model is applied on an example IEC 61499 application. The paper compares the verification results of this IEC 61499 application with two-stage synchronous execution model and the same application with cyclic execution model presented in the earlier work. With this comparison, we verify the portability of the IEC61499 applications across different platforms.

Place, publisher, year, edition, pages
New York: Encyclopedia of Global Archaeology/Springer Verlag, 2015. p. 300-315
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9409
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-33040DOI: 10.1007/978-3-319-25942-0_20Local ID: 7c8dc356-c8b1-4711-a278-5ae470631c3eISBN: 978-3-319-25941-3 (print)ISBN: 978-3-319-25942-0 (electronic)OAI: oai:DiVA.org:ltu-33040DiVA, id: diva2:1006275
Conference
Symposium on Dependable Software Engineering : Theories, Tools and Applications 04/11/2015 - 06/11/2015
Note
Validerad; 2015; Nivå 1; 20151022 (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 text

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: 39 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