Formal modelling of distributed automation CPS with CP-agnostic software

Dmitrii Drozdov, Sandeep Patil*, Valeriy Vyatkin

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterScientificpeer-review

4 Citations (Scopus)


This paper introduces the application of formal modelling to cyber-physical systems for the purpose of formal verification of cyber-physical agnosticism properties of decentralised automation software. Service-oriented cyberphysical systems are modelled using the IEC 61499 function block architecture. Then, the IEC 61499 model is represented in terms of SMV formal language, which is verified using the nuXmv model checker. The timestamped events mechanism is implemented in IEC 61499 using the existing syntax of the standard. The impact of jitter on the behaviour of physical system is demonstrated in both simulation within IEC 61499 execution environment and in counter-examples extracted from nuXmv. The methodology presented in this paper creates the premise for automatic verification of the cyber-physical agnosticism of systems.

Original languageEnglish
Title of host publicationStudies in Computational Intelligence
Place of PublicationCham, Switzerland
Number of pages12
ISBN (Electronic)978-3-319-51100-9
ISBN (Print)978-3-319-51099-6
Publication statusPublished - 2017
MoE publication typeA3 Part of a book or another research book
EventInternational Workshop on Service Orientation in Holonic and Multi-Agent Manufacturing - New University of Lisbon, Lisbon, Portugal
Duration: 6 Oct 20167 Oct 2016

Publication series

NameStudies in Computational Intelligence
ISSN (Print)1860-949X


WorkshopInternational Workshop on Service Orientation in Holonic and Multi-Agent Manufacturing
Abbreviated titleSOHOMA


  • Cyber physical systems
  • Distributed automation systems
  • Formal verification
  • IEC 61499
  • NuXmv
  • SOA


Dive into the research topics of 'Formal modelling of distributed automation CPS with CP-agnostic software'. Together they form a unique fingerprint.

Cite this