工业控制系统的正确可靠对经济发展、人身安全和社会稳定有着重要意义。工业控制系统面对的一个基本问题是控制中的时序问题。如何从时序规约(specification)自动生成满足该规约的程序是学术界长期关注的问题。现有工作中,通常通过线性时序逻辑(LTL)和计算树逻辑(CTL)等方式表达时序规约,通过自动机上的博弈技术和模型检验技术生成满足这些规约的程序,生成的程序具有最坏指数级的规模,不够实用。Matthew B.Dwyer等人总结了一个包含55种模式的时序规约模式系统(SPS),可以描述工业界大多数常见时序规约。本文针对SPS规约模式,实现了线性规模的程序生成。由于PLC(可编程逻辑控制器)在工业控制中得到广泛应用,本文以PLC语言为目标语言。具体工作包括:(1)SPS的精确语义描述:发现了SPS提出者提供的未来时序逻辑(FIL)定义中,对两个重要的时间范围模式的FIL定义不适用于常见的控制场景。本文给出了反例,提供了新的定义,并对SPS的全套FIL定义进行了证明。(2)PLC的Coq模型:给出了PLC语言的语法、语义在Coq中的定义,该定义体现了PLC程序周期性执行模式下的语义效果,为基于Hoare逻辑的PLC程序正确性证明提供了具有通用性的基础。(3)PLC程序生成:本文在基本SPS规约的基础上,定义了一个SPS规约描述语言,体现了SPS规约描述实际工控系统时可能面对的各种变化。利用SPS的组合特性以及控制层级关系,提出了满足这种规约的PLC程序生成规则,证明了该规则的正确性。证明了利用该规则生成的程序规模为SPS规约的线性规模。文中针对一些典型的工业控制问题,利用以上规则生成了程序,并使用Coq证明了生成结果的正确性。