Formal description of an IEC 61499 runtime environment with real-time constraints

This paper investigates on the introduction of the runtime behavior and real-time constraints into the verification process of IEC 61499 based automation systems. In detail, the event propagation policies as well as the necessary execution time for all actions within the automation system need to be described for a complete model of the automation system. The basis of the formal description provides an analytic methodology for the event propagation policy of an IEC 61499 runtime implementation. By use of this methodology within the formal model of the runtime environment, the overall system behavior can be described also in the case of reactive systems properties.