Model-based generation of modular PLC code using IEC61131 function blocks

Mathematical models and formal methods can be used for verifying/falsifying a discrete event controller just before it is put into operation. If the controller model is verified successfully, one has to translate it into an executable implementation. The complexity of technical systems requires a systematic design of needed models. Usually, modular and hierarchically structured models are the results of such a model design. It makes sense to keep the module structures of the controller model within its implementation. After a short introduction the paper illustrates an appropriate modeling formalism and suitable methods for automatic generation of modular control code for programmable logic controllers (PLC) using IEC61131 function blocks.