C语言具有良好的可移植性， 适合于可编程控制器 （Programmable Logical Controller， PLC） 的嵌入式系统实现和研发； 而定时器在PLC系统负责时序逻辑描述， 具有很重要的作用。文章着重研究如何将PLC结构化文本 （StructuredText， ST） 语言中的定时器转换为C语言程序的问题。介绍了ST定时器时间自动机模型的构建， 以及将该时间自动机描述为C程序， 并采用UPPAAL模型检测工具进行验证， 从而保证转换前后功能的一致性。