Programmable logic controllers (PLCs) are widely used in embedded systems. Timers play a pivotal role in PLC real-time applications. The formalization of timers is of great importance. The study presents a formalization of PLC timers in the theorem proving system Coq, in which the behaviors of timers are characterized by a set of axioms at an abstract level. The authors discuss how to model timers at a proper and sound abstract level. PLC programs with timers are modeled. As a case study, a quiz machine problem with a timer is investigated. This work demonstrates the complexity of formal timer modeling