摘要

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

全文