Formal model of IEC 61499 execution trace in FBME IDE

With increase in use formal verification tools and methods in distributed systems, it is becoming more challenging to analyse the execution traces generated by formal verification tools. This paper presents a method for unification of execution traces of industrial automation systems, based on IEC 61499 standard. Execution trace of a system is a sequence of events, where each event represents a change in the state of the system. Execution traces allow developers to explore safely behavior of control software. Execution traces can be obtained several ways, including monitoring of a real system (or its simulator), or as a counterexample build by model checker. In the paper we explore unification of execution traces for debug task in FBME - modular IDE for IEC 61499 applications. We present the formal model of the execution trace representation and show the working on a simple example.