In this paper, we focus on modeling and verification of PLC systems, which are widespread in industry and manufacture. Our approach is based on a translation procedure from PLC programs to timed automata. The resulting model consists of several kinds of modules. Besides of the main module which depicts the behaviors of the PLC programs, a dedicated module is constructed to be accord with the cyclical running mode of PLC systems, and another module is involved for specifying the environment behaviors. After all modules constructed, the model checker Uppaal is adapted to perform the model checking. Experimental results show promising performance of our approach. Comparing to existing approaches, extensive instructions are supported in this paper, including not only the time-related instructions, such as timer and counter, but also the subroutine and interruption instructions. In addition, the structure of whole model is more compact, and the translation procedure is more efficient, which results in a reduced verification model.