Modelling and verification of program logic controllers using timed automata

Validation is an important task in complex embedded system designs. A method of modelling and analysing embedded systems with programmable logic controllers is presented. Controllers and physical plants are modelled using timed automata. The system requirements are specified and formalised as computational tree logic properties. It is demonstrated that the designed model satisfies the required properties by resorting to a symbolic model checker, Uppaal, for real-time systems. A realistic example, the steeve controller of a theatre, illustrates the strategies. The safety and time constraint requirements are validated by Uppaal. The experimental results demonstrate the effectiveness of the approach presented here.