Programmable logic controllers (PLCs) are widely used in computer-based industrial applications. Timers play a pivotal role in PLC real-time embedded system applications. The paper addresses the formal validation of PLC systems with timers in the theorem proving system Coq. The timer behavior is characterized formally. A refinement validation methodology is presented in terms of an abstract model and a concrete model. The refinement is calibrated by a mapping relation. The soundness of the methodology is shown in the proving system. An illustrative case study demonstrates the eectiveness of the approach.