SMT-based deployment calculation for IEC 61499 control applications

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.