Functional and temporal formal modelling of embedded controllers for intelligent mechatronic systems

Formal verification of intelligent mechatronic systems needs to incorporate a detailed description of the system architecture in order to provide sufficient results. Especially • the model of function blocks with precise semantics • real-time behaviour has to be included. This paper focuses on the IEC 61499 control applications for automation objects, the building blocks for intelligent mechatronic systems. A comprehensive approach for their formal description of control behaviour incorporating also the operating system policy and physical time as parameter for real-time behaviour is given on the basis of Net Condition/Event Systems for a typical control device configuration.