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 cyber-physical automation systems modelled with timed block diagrams
Penza State University.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.
Penza State University.
Penza State University.
Number of Authors: 4
2016 (English)In: IEEE International Symposium on Industrial Electronics, ISIE 2016, Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2016, 316-321 p., 7744910Conference paper (Refereed)
Abstract [en]

In this paper a new modelling approach is presented to be used for formal-verification of block-diagram executable specifications of distributed industrial cyber-physical systems following the IEC 61499 standard. The approach allows usage of timers and arithmetic operations in the controller code. SMV model-checker is used as the target tool. The function block modelswith multiple communicating plant-controller closed-loops are transformed to the SMV modelling language using a dedicated model-generator tool. The paper first deals with SMV modelling of the IEC 61499 specific timer function block types. In particular, modelling of hierarchical function block systems with timers located at different levels of hierarchy is addressed. The paper then presents plant abstraction techniques so that the complexity of cyber-physical systems models is reduced. The abstraction uses discrete-timed state machine model implemented in UPPAAL. Delays in the plant model are interpreted as model time constraints. The approach is illustrated with an example of formal verification of a modular mechatronic automated system. The achieved results extend the abilities in validation of real cyber-physical automation systems. The paper also demonstrates how this result helps in counterexample guided simulation in Ciros 3D simulation environment, which improves practical usability of formal verification

Place, publisher, year, edition, pages
Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2016. 316-321 p., 7744910
Series
Proceedings of the IEEE International Symposium on Industrial Electronics, ISSN 2163-5137
National Category
Computer Science
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-61160DOI: 10.1109/ISIE.2016.7744910ISI: 000390697400045ScopusID: 2-s2.0-85001086083ISBN: 9781509008735 (print)OAI: oai:DiVA.org:ltu-61160DiVA: diva2:1058080
Conference
25th IEEE International Symposium on Industrial Electronics, ISIE 2016, Santa Clara, United States, 8-10 June 2016
Available from: 2016-12-20 Created: 2016-12-20 Last updated: 2017-01-23Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

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