Formal Verification of Cyber-Physical Automation Systems Modelled with Timed Block Diagrams

Dmitrii Drozdov*, Sandeep Patil, Victor Dubinin, Valeriy Vyatkin

*Corresponding author for this work

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

7 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationProceedings of the 25th IEEE International Symposium on Industrial Electronics, ISIE 2016
Number of pages6
ISBN (Electronic)978-1-5090-0873-5
Publication statusPublished - 2016
MoE publication typeA4 Article in a conference publication
EventInternational Symposium on Industrial Electronics - Santa Clara, United States
Duration: 8 Jun 201610 Jun 2016
Conference number: 24

Publication series

NameProceedings of the IEEE International Symposium on Industrial Electronics
ISSN (Print)2163-5137


ConferenceInternational Symposium on Industrial Electronics
Abbreviated titleISIE
Country/TerritoryUnited States
CitySanta Clara
Internet address


  • Cyber-physical systems
  • formal verification
  • model-checking
  • timed formalisms
  • IEC 61499
  • SMV


Dive into the research topics of 'Formal Verification of Cyber-Physical Automation Systems Modelled with Timed Block Diagrams'. Together they form a unique fingerprint.

Cite this