PLCs (Programmable Logic Controllers) are being used increasingly for safety critical applications. Our aim is verification and testing of PLC applications. We consider timing aspects as an integral part of control as performed by PLCs. Timed automata provide a useful class of models, first, because they allow to model real time. Second, because of the availability of models checking tools. We introduce two different models that differ in the way of the treating timers. Both models satisfy the same specification for timing behavior, which indicates that they are interchangeable.
PLCs have evolved from very simple “Logic Controllers” that used to control physical processes by feeding the input from the sensors via a carefully designed network of timers and relays to the actuators. PLCs are programmable: they contain a microprocessor so that a computer program so that a computer program can perform the task of the timers and the switches of their forefathers. Although modern PLCs can contain the same processor chip as a usual desktop computer they differ from, say, personal computers in number of aspects.
• They are programmed by means of notations and languages, which are unfamiliar to most computer scientist, while vice versa, many useful concepts that were developed in computer science are unfamiliar to the engineers who program PLCs.
• Real time behavior is ensured using the conceptually very simple timers. These can either be realized as hardware components or be simulated by pieces of software.
• They have a robust operating system, which ensures that scan cycles are executed again. In each scan cycle the actual PLC program is executed, input is polled and the output is updated once before each program execution.
There are more complex PLCs, which support interrupts and multi tasking. They are more difficult to verify although some find them easier to program. These powerful features are not strictly necessary for many applications.