Formal Verification of IEC 61499 Enhanced with Timed Events

Viktor Shatrov*, Valeriy Vyatkin

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


Many applications of Cyber-Physical Systems (CPS) play a crucial role in shaping the quality of life. The malfunction of such systems can lead to dangerous consequences, hence safety takes an important role. One of the common issues of CPS is the variability of event delays. This paper addresses formal verification of system ability to withstand event delays. To achieve such property, we use the concept of event timestamps. The paper proposes changes in IEC 61499 syntax to introduce timestamps into the programming language. The application of new syntax introduces better opportunities for formal verification. We enhanced FB2SMV tool to generate SMV models automatically from the initial system. The paper presents a case study of an elevator system that illustrates the proposed approach. Results of verification show that the system can perform time-aware computations. The proposed approach has shown better verification performance compared to timestamps manually added through the data connections between function blocks.

Original languageEnglish
Title of host publicationProceedings of the 11th IFIP WG 5.5/SOCOLNET Advanced Doctoral Conference on Computing, Electrical and Industrial Systems, Technological Innovation for Life Improvement, DoCEIS 2020
EditorsLuis M. Camarinha-Matos, Nastaran Farhadi, Fábio Lopes, Helena Pereira
Number of pages11
Publication statusPublished - 2020
MoE publication typeA4 Article in a conference publication
EventAdvanced Doctoral Conference on Computing, Electrical and Industrial Systems - Costa de Caparica, Portugal
Duration: 1 Jul 20203 Jul 2020
Conference number: 11

Publication series

NameIFIP Advances in Information and Communication Technology
ISSN (Print)1868-4238
ISSN (Electronic)1868-422X


ConferenceAdvanced Doctoral Conference on Computing, Electrical and Industrial Systems
Abbreviated titleDoCEIS
CityCosta de Caparica


  • Cyber-physical systems
  • Formal verification
  • IEC 61499
  • Time-aware computations

Fingerprint Dive into the research topics of 'Formal Verification of IEC 61499 Enhanced with Timed Events'. Together they form a unique fingerprint.

Cite this