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

北京大学学报（自然科学版）

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

陈钢¹,宋晓宇², 顾明³

1. Lingcore Laboratory, Portland, OR97224; 2.Department of ECE, Portland State University, Portland, OR97207; 3. 清华大学软件学院, 北京100084;

收稿日期:2009-01-05 出版日期:2010-01-20 发布日期:2010-01-20

PLC Program Verification and Analysis Using the COQ Theorem Prover

CHEN Gang¹, SONG Xiaoyu², GU Ming³

1. Lingcore Laboratory, Portland, OR97224; 2. Department of ECE, Portland State University, Portland, OR97207; 3.School of Software, Tsinghua University, Beijing 100084;

Received:2009-01-05 Online:2010-01-20 Published:2010-01-20

摘要/Abstract

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

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

Abstract: 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 theseresults the author sintroducethe 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.

Key words: programmable logic controller, PLC, embedded system, COQ, the oremproving

中图分类号:

TP301

陈钢,宋晓宇, 顾明. COQ定理证明器辅助PLC 程序验证和分析[J]. 北京大学学报（自然科学版）.

CHEN Gang,SONG Xiaoyu,GU Ming. PLC Program Verification and Analysis Using the COQ Theorem Prover[J]. Acta Scientiarum Naturalium Universitatis Pekinensis.

导出引用管理器 EndNote|Ris|BibTeX

链接本文: https://xbna.pku.edu.cn/CN/

https://xbna.pku.edu.cn/CN/Y2010/V46/I1/30

[1]	武玲娟,崔小欣,于敦山. 水下声学调制解调器动态可重构数字系统设计与实现[J]. 北京大学学报（自然科学版）, 2013, 49(5): 765-772.
[2]	刘晓瑜,孙樯. PLC自动控制系统在常规⁴⁰Ar/³⁹Ar同位素定年系统纯化部分中的应用[J]. 北京大学学报（自然科学版）, 2012, 48(6): 879-885.
[3]	李皓,郑衍松,庞九凤,佟冬,程旭. EmBIOS: 一种支持MS Windows的嵌入式系统BIOS设计[J]. 北京大学学报（自然科学版）, 2012, 48(1): 20-28.
[4]	李莹,Bridget Benson,于敦山,Ryan Kastner,张兴. 使用嵌入式处理器的水声调制解调器控制系统设计方法与研究[J]. 北京大学学报（自然科学版）, 2011, 47(2): 245-250.
[5]	滕启明, 陈向群. XCODE: 一种面向系统软件的可扩展构件描述语言[J]. 北京大学学报（自然科学版）, 2004, 40(3): 388-396.