SMT-based deployment calculation for IEC 61499 control applications

Tuojian Lyu, Jan Olaf Blech, Valeriy Vyatkin

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

1 Citation (Scopus)
78 Downloads (Pure)


The dynamic and flexible deployment optimization of industrial control applications is essential for achieving the goals of Smart Factories and Industry 4.0. In this paper, we are studying distributed IEC 61499 control applications. To achieve the required efficiency and flexibility of the control application deployment, we propose using a Satisfiability Modulo Theories (SMT) solver to solve the underlying redeployment model constraints. In our work the Z3 solver is used for this purpose. The proposed redeployment models represent the redeployment problem and allow the Z3 solver to efficiently and quickly calculate the optimization result. Furthermore, based on the Z3 solver APIs, several critical components of the redeployment architecture (Monitor, Parser, Generator, etc.) are implemented in Java applications. The experiment results indicate that, based on our implemented Z3-based software and redeployment models, the deployment optimization results can be quickly obtained for simple IEC 61499 applications.

Original languageEnglish
Title of host publicationProceedings of 4th IEEE International Conference on Industrial Cyber-Physical Systems, ICPS 2021
Number of pages7
ISBN (Electronic)9781728162072
Publication statusPublished - 5 Jul 2021
MoE publication typeA4 Conference publication
EventInternational Conference on Industrial Cyber-Physical Systems - Virtual, Online
Duration: 10 May 202113 May 2021
Conference number: 4


ConferenceInternational Conference on Industrial Cyber-Physical Systems
Abbreviated titleICPS
CityVirtual, Online


  • Containerization
  • Flexible redeployment
  • IEC 61499
  • Satisfiability modulo theories
  • Smart factory


Dive into the research topics of 'SMT-based deployment calculation for IEC 61499 control applications'. Together they form a unique fingerprint.

Cite this