Functional and temporal formal modelling of embedded controllers for intelligent mechatronic systems. (2nd April 2009) - Sunder, Christoph; Vyatkin, Valeriy
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.