SMT-Based Deployment Calculation in Industrial Automation Domain

Tarik Terzimehić, Monika Wenger, Sebastian Voss, Sten Grüner und Haitham Elfham

Proceedings of the IEEE International Conference on Emerging Technologies And Factory Automation (ETFA),

September 2019


The desired flexibility of industrial automation systems foresees among others flexible deployment and execution of control applications on distributed control nodes. This task can be performed more efficiently by an automated deployment algorithm yielding a valid deployment and optimizing nonfunctional objectives. Although extensively investigated, automated deployment approaches for the automotive domain cannot be translated to industrial control applications, due to a different execution semantics. Thus, in this paper, we present a method of satisfiability modulo theories (SMT)-based automated deployment of the industrial automation systems. We formalize and implement domain-relevant constraints and objectives. Our contribution is threefold: 1) we formalize the functional coupling and end-to-end deadline constraints and objectives while considering the semantics of control applications, 2) we encode the deployment problem into an SMT form, and 3) we validate the approach on an abstract example and a domain-relevant use case. The results obtained in this paper will allow application engineers to fulfill functional and real-time requirements by automatically solving the deployment problem.

Stichworte:basys 4.0, mbse