COQ定理证明器辅助PLC程序验证和分析

摘要：

使用定理证明器COQ验证和分析PLC抢答器程序的一些性质,证明了原程序的所有可能状态中只有半数是可达状态,揭示了系统在可达状态之间的转移关系.基于这些性质,引入了逻辑自动机的概念作为对PLC程序行为完整抽象的描述.此外,在证明过程中,发现该程序中存在着一个很难通过现场测试发现的问题.

关键词：可编程序控制器、PLC、嵌入式系统、COQ、定理证明

所属期刊栏目：46

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目90718039

在线出版日期：2017-01-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：30-34