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

PLC Program Verification and Analysis Using the COQ Theorem Prover

作　　者：陈钢 宋晓宇 顾明[3] 

机构地区：[1]Lingcore Laboratory,Portland,or97224 [2]Department of ECE,Portland State University,Portland,or97207 [3]清华大学软件学院,北京100084

出　　处：《北京大学学报（自然科学版）》2010年第1期30-34,共5页Acta Scientiarum Naturalium Universitatis Pekinensis

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

摘　　要：使用定理证明器COQ验证和分析PLC抢答器程序的一些性质,证明了原程序的所有可能状态中只有半数是可达状态,揭示了系统在可达状态之间的转移关系。基于这些性质,引入了逻辑自动机的概念作为对PLC程序行为完整抽象的描述。此外,在证明过程中,发现该程序中存在着一个很难通过现场测试发现的问题。The authors analyse a PLC competition quiz machine program and proves a set of properties using the COQ theorem prover.These properties reveal that only half of output states would be reachable and describe the transition relation over these states in an abstract way.Based on these results the authors introduce the notion of logic automata as a complete description of this PLC program.The authors also point out that the program may produce unfair response in rare situations.

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

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]